Commit 2021-02-04 03:30 cbd67cf4

View on Github →

feat(order/(complete_lattice, compactly_generated)): independent sets in a complete lattice (#5971) Defines complete_lattice.independent Shows that this notion of independence is finitary in compactly generated lattices

Estimated changes

Modified src/order/compactly_generated.lean

added theorem Sup_compact_le_eq

added theorem complete_lattice.independent_iff_finite

added theorem inf_Sup_eq_of_directed_on

added theorem inf_Sup_eq_supr_inf_sup_finset

added theorem le_iff_compact_le_imp

Modified src/order/complete_boolean_algebra.lean

Modified src/order/complete_lattice.lean

added theorem complete_lattice.independent.mono

added def complete_lattice.independent

added theorem sup_Inf_le_infi_sup

added theorem supr_inf_le_inf_Sup