Theorem Function.not_lt_argminOn

Modification history

2026-03-15 15:56

Mathlib/Order/WellFounded.lean

chore(WellFounded): drop unneeded `Set.Nonempty` assumptions (#35933) …

Modified Function.not_lt_argminOn View on Github →

2022-12-13 21:24

Mathlib/Order/WellFounded.lean

feat port: Order.WellFounded (#970) …

Added Function.not_lt_argminOn View on Github →