Commit 2025-01-26 10:39 150682c4

View on Github →

refactor(Order/WellFounded): use WellFoundedLT for argmin (#20777) Instead of taking an explicit WellFounded (· < ·) argument, we can take a typeclass WellFoundedLT argument instead.

Estimated changes

Modified Mathlib/Analysis/Convex/Caratheodory.lean

Modified Mathlib/CategoryTheory/CofilteredSystem.lean

Modified Mathlib/Order/ConditionallyCompleteLattice/Basic.lean

modified theorem sInf_eq_argmin_on

Modified Mathlib/Order/WellFounded.lean

modified theorem Function.argminOn_mem

modified theorem Function.argmin_le

modified theorem Function.not_lt_argmin