Theorems · Inductive type · order theory
CompleteSemilatticeSup
Type u_8 → Type u_8
Note that we rarely use CompleteSemilatticeSup
(in fact, any such object is always a CompleteLattice, so it's usually best to start there).
Nevertheless it is sometimes a useful intermediate step in constructions.
- Defined in
- Mathlib.Order.CompleteLattice.Defs
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 0 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by28
Results whose statement or proof uses this declaration.
- le_sSupstatement and proof · cited by 79
- sSup_lestatement and proof · cited by 35
- sSup_le_sSupstatement and proof · cited by 24
- isLUB_sSupstatement and proof · cited by 21
- IsLUB.sSup_eqstatement and proof · cited by 17
- le_iSup_iffstatement and proof · cited by 16
- sSup_singletonstatement and proof · cited by 14
- sSup_le_iffstatement and proof · cited by 8
- isLUB_iff_sSup_eqstatement and proof · cited by 3
- iSup_lt_iffstatement and proof · cited by 2
- le_sSup_of_lestatement and proof · cited by 2
- CompleteSemilatticeSup.isLUB_sSupstatement and proof · cited by 1