Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-10 17:59 b72811f2

View on Github →

feat(order/complete_well_founded): characterise well-foundedness for complete lattices (#5575)

Estimated changes

Created src/order/complete_well_founded.lean

added theorem complete_lattice.is_Sup_finite_compact.is_sup_closed_compact

added def complete_lattice.is_Sup_finite_compact

added theorem complete_lattice.is_Sup_finite_compact_iff_is_sup_closed_compact

added theorem complete_lattice.is_sup_closed_compact.well_founded

added def complete_lattice.is_sup_closed_compact

added theorem complete_lattice.is_sup_closed_compact_iff_well_founded

added theorem complete_lattice.well_founded.is_Sup_finite_compact

added theorem complete_lattice.well_founded_characterisations

added theorem complete_lattice.well_founded_iff_is_Sup_finite_compact