Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 00:37 030107f6

View on Github →

feat(order/compactly_generated): A compactly-generated modular lattice is complemented iff atomistic (#6071) Shows that a compactly-generated modular lattice is complemented iff it is atomistic Proves extra lemmas about atomistic or compactly-generated lattices Proves extra lemmas about complete_lattice.independent Fix the name of is_modular_lattice.sup_inf_sup_assoc

Estimated changes

Modified docs/references.bib

Modified src/order/atoms.lean

added theorem Sup_atoms_eq_top

added theorem Sup_atoms_le_eq

added theorem le_iff_atom_le_imp

Modified src/order/compactly_generated.lean

added theorem Sup_compact_eq_top

added theorem complete_lattice.independent_Union_of_directed

added theorem complete_lattice.independent_sUnion_of_directed

added theorem is_complemented_iff_is_atomistic

added theorem is_complemented_of_is_atomistic

Modified src/order/complete_lattice.lean

added theorem Sup_sUnion

added theorem complete_lattice.independent_empty

Modified src/order/modular_lattice.lean

added theorem disjoint.disjoint_sup_right_of_disjoint_sup_left

added theorem is_modular_lattice.inf_sup_inf_assoc

added theorem is_modular_lattice_iff_inf_sup_inf_assoc

deleted theorem is_modular_lattice_iff_sup_inf_sup_assoc