Commit 2023-01-21 16:46 1ec531b5

View on Github →

feat: port Order.ConditionallyCompleteLattice.Finset (#1748)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Finset.Nonempty.cInf_eq_min'

added theorem Finset.Nonempty.cInf_mem

added theorem Finset.Nonempty.cSup_eq_max'

added theorem Finset.Nonempty.cSup_mem

added theorem Finset.Nonempty.sup'_eq_cSup_image

added theorem Finset.Nonempty.sup'_id_eq_cSup

added theorem Finset.inf'_eq_cInf_image

added theorem Finset.inf'_id_eq_cInf

added theorem Finset.sup'_eq_cSup_image

added theorem Finset.sup'_id_eq_cSup

added theorem Set.Finite.cSup_lt_iff

added theorem Set.Finite.lt_cInf_iff

added theorem Set.Nonempty.cInf_mem

added theorem Set.Nonempty.cSup_mem