Structures · Order
IsCompactlyGenerated
A complete lattice is said to be compactly generated if any
element is the sSup of compact elements.
- Defined in
- Mathlib.Order.CompactlyGenerated.Basic
- Shape
- One type argument · adds exists_sSup_eq
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances4
- LieSubmodule
- Set.Elem
- Submodule
- IntermediateField
How is a type an instance?
Loading the hierarchy index…
Assumed by43
- inf_sSup_eq_iSup_inf_sup_finset
- IsCompactlyGenerated.BooleanGenerators.atomistic
- IsCompactlyGenerated.BooleanGenerators.mem_of_isAtom_of_le_sSup_atoms
- complementedLattice_of_sSup_atoms_eq_top
- DirectedOn.inf_sSup_eq
- sSup_compact_le_eq
- exists_sSupIndep_disjoint_sSup_atoms
- complementedLattice_of_isAtomistic
- IsCompactlyGenerated.exists_sSup_eq
- le_iff_compact_le_imp
- iSupIndep_iff_supIndep
- DirectedOn.sSup_inf_eq
- complementedLattice_of_complementedLattice_Iic
- Directed.iSup_inf_eq
- exists_sSupIndep_of_sSup_atoms_eq_top
- iSupIndep.disjoint_biSup_biSup
- exists_sSupIndep_of_sSup_atoms
- DirectedOn.disjoint_sSup_right
- IsCompactlyGenerated.BooleanGenerators.distribLatticeOfSSupEqTop
- exists_sSupIndep_isCompl_sSup_atoms
- disjoint_biSup_of_finite_disjoint_biSup
- sSupIndep_iff_finite
- sSupIndep_iUnion_of_directed
- Directed.inf_iSup_eq
- complementedLattice_iff_isAtomistic
- Directed.disjoint_iSup_right
- iSupIndep_sUnion_of_directed
- IsCompactlyGenerated.BooleanGenerators.isAtomistic_of_sSup_eq_top
- Directed.disjoint_iSup_left
- Set.Iic.instIsCompactlyGenerated
- iSupIndep_iff_supIndep_of_injOn
- isAtomistic_of_complementedLattice
- IsCompactlyGenerated.BooleanGenerators.sSup_le_sSup_iff_of_atoms
- IsCompactlyGenerated.BooleanGenerators.booleanAlgebraOfSSupEqTop
- iSupIndep.iInf
- isAtomic_of_complementedLattice
- IsCompactlyGenerated.BooleanGenerators.booleanAlgebra_of_sSup_eq_top
- IsCompactlyGenerated.BooleanGenerators.distribLattice_of_sSup_eq_top
- IsCompactlyGenerated.BooleanGenerators.eq_atoms_of_sSup_eq_top
- IsCompactlyGenerated.BooleanGenerators.sSup_inter
- IsCompactlyGenerated.BooleanGenerators.complementedLattice_of_sSup_eq_top
- DirectedOn.disjoint_sSup_left
- sSup_compact_eq_top
Ancestors0
No ancestors.