Theorems · Inductive type · order theory
IsCompactlyGenerated
(α : Type u_3) → [CompleteLattice α] → Prop
A complete lattice is said to be compactly generated if any
element is the sSup of compact elements.
- Defined in
- Mathlib.Order.CompactlyGenerated.Basic
- Cited by
- 37 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CompleteLattice
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CompleteLatticestatement · cited by 1,048
Cited by43
Results whose statement or proof uses this declaration.
- inf_sSup_eq_iSup_inf_sup_finsetstatement and proof · cited by 4
- IsCompactlyGenerated.BooleanGenerators.atomisticstatement and proof · cited by 4
- complementedLattice_of_sSup_atoms_eq_topstatement and proof · cited by 3
- IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atomsstatement and proof · cited by 3
- DirectedOn.inf_sSup_eqstatement and proof · cited by 3
- exists_sSupIndep_disjoint_sSup_atomsstatement and proof · cited by 2
- sSup_compact_le_eqstatement and proof · cited by 2
- complementedLattice_of_isAtomisticstatement and proof · cited by 2
- IsCompactlyGenerated.exists_sSup_eqstatement and proof · cited by 2
- iSupIndep_iff_supIndepstatement and proof · cited by 2
- le_iff_compact_le_impstatement and proof · cited by 2
- DirectedOn.sSup_inf_eqstatement and proof · cited by 2