Commit 2026-08-24 11:53 8aa544b3

View on Github →

chore(Order/WellFounded): use to_dual (#39438) Creates argmax/argmaxOn duals to the existing argmin/argminOn, and WellFoundedLT.min/WellFoundedGT.max in order to properly dualize WellFounded.min_le. Some theorems about WellFounded{LT/GT} which didn't have a dual before have to be renamed to make room, e.g. StrictMono.range_inj is renamed to StrictMono.range_inj_of_wellFoundedLT.

Estimated changes

Modified Mathlib/Data/Finset/Sort.lean

Modified Mathlib/FieldTheory/CardinalEmb.lean

Modified Mathlib/LinearAlgebra/Matrix/Determinant/Bird/Correctness.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Defs.lean

Modified Mathlib/Order/Hom/Set.lean

deleted theorem OrderEmbedding.range_inj

added theorem OrderEmbedding.range_inj_of_wellFoundedLT

Modified Mathlib/Order/SuccPred/Basic.lean

Modified Mathlib/Order/UpperLower/Basic.lean

Modified Mathlib/Order/WellFounded.lean

modified theorem Function.argminOn_le

deleted theorem Function.isMinimalFor_argmin

deleted theorem Function.isMinimalFor_argminOn

added theorem Function.minimalFor_argmin

added theorem Function.minimalFor_argminOn

deleted theorem Set.range_injOn_strictAnti

added theorem Set.range_injOn_strictAnti_of_wellFoundedGT

deleted theorem Set.range_injOn_strictMono

added theorem Set.range_injOn_strictMono_of_wellFoundedLT

deleted theorem StrictAnti.range_inj

added theorem StrictAnti.range_inj_of_wellFoundedGT

deleted theorem StrictMono.apply_le

deleted theorem StrictMono.le_id

deleted theorem StrictMono.not_bddBelow_range_of_wellFoundedGT

deleted theorem StrictMono.range_inj

added theorem StrictMono.range_inj_of_wellFoundedLT

modified theorem WellFounded.min_le

added theorem WellFoundedLT.min_le

Modified Mathlib/SetTheory/Cardinal/Cofinality/Enum.lean

Modified Mathlib/SetTheory/Ordinal/Enum.lean