Commit 2026-09-01 10:17 cecebc30

View on Github →

chore(Data/Finset/Max): use to_dual (#43289) This PR uses to_dual on Finset.max and Finset.max'

Estimated changes

deleted theorem Finset.coe_min'
deleted theorem Finset.exists_min_image
deleted theorem Finset.exists_next_left
deleted theorem Finset.induction_on_min
deleted theorem Finset.isLUB_mem
deleted theorem Finset.isLeast_min'
deleted theorem Finset.le_min'
deleted theorem Finset.le_min'_iff
deleted theorem Finset.lt_min'_iff
deleted theorem Finset.map_ofDual_min
deleted theorem Finset.map_toDual_min
modified theorem Finset.max'_insert
deleted theorem Finset.mem_of_min
deleted def Finset.min'
deleted theorem Finset.min'_eq_iff
deleted theorem Finset.min'_eq_inf'
deleted theorem Finset.min'_erase_ne_self
deleted theorem Finset.min'_image
deleted theorem Finset.min'_insert
deleted theorem Finset.min'_le
deleted theorem Finset.min'_mem
deleted theorem Finset.min'_pair
deleted theorem Finset.min'_singleton
deleted theorem Finset.min'_subset
deleted theorem Finset.min'_union
deleted theorem Finset.min_empty
deleted theorem Finset.min_eq_inf_withTop
deleted theorem Finset.min_eq_top
deleted theorem Finset.min_erase_ne_self
deleted theorem Finset.min_insert
deleted theorem Finset.min_le
deleted theorem Finset.min_le_of_eq
deleted theorem Finset.min_mem_image_coe
deleted theorem Finset.min_mono
deleted theorem Finset.min_of_mem
deleted theorem Finset.min_of_nonempty
deleted theorem Finset.min_pair
deleted theorem Finset.min_singleton
deleted theorem Finset.min_union
deleted theorem Finset.notMem_of_lt_min
deleted theorem Finset.ofDual_min'
deleted theorem Finset.toDual_min'
deleted theorem Monotone.map_finset_min'
deleted theorem Multiset.exists_min_image