Commit 2023-02-01 13:07 3a0c3c19

View on Github →

feat: port Order.CompactlyGenerated (#1976) Missing tactics:

Tfae
change .. with

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/CompactlyGenerated.lean

added theorem CompleteLattice.Iic_coatomic_of_compact_element

added theorem CompleteLattice.IsCompactElement.directed_supₛ_lt_of_lt

added theorem CompleteLattice.IsCompactElement.exists_finset_of_le_supᵢ

added def CompleteLattice.IsCompactElement

added theorem CompleteLattice.IsSupClosedCompact.wellFounded

added def CompleteLattice.IsSupClosedCompact

added theorem CompleteLattice.IsSupFiniteCompact.isSupClosedCompact

added def CompleteLattice.IsSupFiniteCompact

added theorem CompleteLattice.WellFounded.finite_of_independent

added theorem CompleteLattice.WellFounded.finite_of_setIndependent

added theorem CompleteLattice.WellFounded.isSupFiniteCompact

added theorem CompleteLattice.coatomic_of_top_compact

added theorem CompleteLattice.finset_sup_compact_of_compact

added theorem CompleteLattice.independent_unionₛ_of_directed

added theorem CompleteLattice.isCompactElement_iff.{u}

added theorem CompleteLattice.isCompactElement_iff_le_of_directed_supₛ_le

added theorem CompleteLattice.isCompactlyGenerated_of_wellFounded

added theorem CompleteLattice.isSupClosedCompact_iff_wellFounded

added theorem CompleteLattice.isSupFiniteCompact_iff_all_elements_compact

added theorem CompleteLattice.isSupFiniteCompact_iff_isSupClosedCompact

added theorem CompleteLattice.setIndependent_iff_finite

added theorem CompleteLattice.setIndependent_unionᵢ_of_directed

added theorem CompleteLattice.wellFounded_characterisations

added theorem CompleteLattice.wellFounded_iff_isSupFiniteCompact

added theorem complementedLattice_iff_isAtomistic

added theorem complementedLattice_of_isAtomistic

added theorem complementedLattice_of_supₛ_atoms_eq_top

added theorem inf_supₛ_eq_of_directedOn

added theorem inf_supₛ_eq_supᵢ_inf_sup_finset

added theorem le_iff_compact_le_imp

added theorem supₛ_compact_eq_top

added theorem supₛ_compact_le_eq