Commit 2023-04-20 22:04 e8cf0cfe

View on Github →

feat(order/compactly_generated): For any b, there exists a set of independent atoms s such that Sup s is the complement of b. (#8475) This new lemma is carved out of the proof that atomistic lattices are complemented. Also provide directed versions of the interaction between suprema and disjointness.

Estimated changes

Modified src/order/compactly_generated.lean

added theorem directed_on.inf_Sup_eq

added theorem exists_set_independent_is_compl_Sup_atoms

added theorem exists_set_independent_of_Sup_atoms_eq_top

deleted theorem inf_Sup_eq_of_directed_on

Modified src/order/directed.lean

modified theorem directed_on_range