Commit 2024-09-02 15:27 67ce578d

View on Github →

feat(ConditionallyCompleteLattice/Finset): ciSup_mem on list/multiset/finset (#15284) As well as toDual_csSup And simpler lemmas when on ConditionallyCompleteLinearOrderBot

Estimated changes

Modified Mathlib/Order/CompleteLattice.lean

modified theorem ofDual_iInf

modified theorem ofDual_iSup

modified theorem ofDual_sInf

modified theorem ofDual_sSup

modified theorem toDual_iInf

modified theorem toDual_iSup

modified theorem toDual_sInf

modified theorem toDual_sSup

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

added theorem Finset.Nonempty.ciSup_eq_max'_image

added theorem Finset.Nonempty.ciSup_mem_image

added theorem Finset.ciInf_eq_min'_image

added theorem Finset.ciInf_mem_image

added theorem Finset.ciSup_eq_max'_image

added theorem Finset.ciSup_mem_image

added theorem List.iInf_mem_map_of_exists_le_sInf_empty

added theorem List.iSup_mem_map_of_exists_sSup_empty_le

added theorem List.iSup_mem_map_of_ne_nil

added theorem Multiset.iInf_mem_map_of_exists_le_sInf_empty

added theorem Multiset.iSup_mem_map_of_exists_sSup_empty_le

added theorem Multiset.iSup_mem_map_of_ne_zero

added theorem Set.Finite.ciInf_mem_image

added theorem Set.Finite.ciSup_lt_iff

added theorem Set.Finite.ciSup_mem_image

added theorem Set.Finite.lt_ciInf_iff

added theorem Set.Nonempty.ciSup_lt_iff

added theorem Set.Nonempty.ciSup_mem_image