Theorems · Theorem · order theory
IsGLB.unique
∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsGLB s a → IsGLB s b → a = b- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 13 results in Mathlib
- Foundations
- Depth 7 from the axioms · uses no axioms
- Assumes
- PartialOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement and proof · cited by 53,352
- PartialOrderstatement and proof · cited by 6,410
- IsGLBstatement and proof · cited by 213
- IsGreatest.uniqueproof · cited by 6
Cited by13
Results whose statement or proof uses this declaration.
- GaloisConnection.u_infproof · cited by 37
- IsGLB.csInf_eqproof · cited by 13
- IsLeast.csInf_eqproof · cited by 11
- GaloisConnection.u_csInf_of_directedOn'proof · cited by 2
- csInf_upperBounds_eq_csSupproof · cited by 2
- sInf_upperBounds_eq_sSupproof · cited by 2
- Sion.minimaxproof · cited by 2
- RightOrdContinuous.map_infproof · cited by 1
- CountableInfClosed.of_iInf_memproof · cited by 1
- CountableInfClosed.singletonproof · cited by 1
- isGLB_iff_sInf_eqproof · cited by 1
- Order.isGLB_Ioi_iff_isPredPrelimitproof · cited by 0