Theorems · Theorem · order theory
IsLUB.unique
∀ {α : Type u_1} [inst : PartialOrder α] {s : Set α} {a b : α}, IsLUB s a → IsLUB s b → a = b- Defined in
- Mathlib.Order.Bounds.Basic
- Cited by
- 21 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
- IsLUBstatement and proof · cited by 280
- IsLeast.uniqueproof · cited by 3
Cited by21
Results whose statement or proof uses this declaration.
- GaloisConnection.l_supproof · cited by 81
- IsLUB.csSup_eqproof · cited by 19
- IsGreatest.csSup_eqproof · cited by 9
- Order.IsNormal.ext_iffproof · cited by 4
- isLUB_iff_sSup_eqproof · cited by 3
- Order.IsNormal.dirSupClosed_rangeproof · cited by 2
- Dense.ciSupproof · cited by 2
- GaloisConnection.l_csSup_of_directedOn'proof · cited by 2
- Function.semiconj_of_isLUBproof · cited by 2
- sSup_lowerBounds_eq_sInfproof · cited by 1
- csSup_lowerBounds_eq_csInfproof · cited by 1
- CountableSupClosed.of_iSup_memproof · cited by 1