Commit 2026-09-03 15:14 9bdf763d

View on Github →

chore(Order/ConditionallyCompleteLattice/Finset): use to_dual (#43320) This PR uses to_dual in Order/ConditionallyCompleteLattice/Finset.

Estimated changes

Modified Mathlib/Algebra/Tropical/BigOperators.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Finset.lean

deleted theorem Finset.Nonempty.csInf_eq_min'

deleted theorem Finset.Nonempty.csInf_mem

deleted theorem Finset.ciInf_eq_min'_image

deleted theorem Finset.ciInf_mem_image

deleted theorem Finset.inf'_eq_csInf_image

deleted theorem Finset.inf'_id_eq_csInf

deleted theorem Finset.inf'_univ_eq_ciInf

deleted theorem List.iInf_mem_map_of_exists_le_sInf_empty

deleted theorem Multiset.iInf_mem_map_of_exists_le_sInf_empty

deleted theorem Set.Finite.ciInf_mem_image

deleted theorem Set.Finite.lt_ciInf_iff

deleted theorem Set.Finite.lt_csInf_iff

deleted theorem Set.Finite.map_sInf_of_monotone

modified theorem Set.Finite.map_sSup_of_monotone

deleted theorem Set.Nonempty.csInf_mem

deleted theorem ciInf_eq_ciInf_finset

deleted theorem exists_eq_ciInf_of_finite

deleted theorem iInf_ne_bot

deleted theorem iInf_ne_of_notMem

deleted theorem sInf_ne_bot

deleted theorem sInf_ne_of_notMem