Theorem Function.isMinimalFor_argminOn

Modification history

2026-08-24 11:53
Mathlib/Order/WellFounded.lean
chore(Order/WellFounded): use `to_dual` (#39438) …
Deleted Function.isMinimalFor_argminOnView on Github →
2025-12-23 14:46
Mathlib/Order/WellFounded.lean
feat: connect `MinimalFor` and `Function.argmin` (#33207)
Added Function.isMinimalFor_argminOnView on Github →