Theorem Set.IsWF.min_eq_of_le

Modification history

2024-11-13 21:29
Mathlib/Order/WellFoundedSet.lean
feat(Order/WellFoundedSet): sufficient conditions for unique minima of well-founded sets (#18977) …
Added Set.IsWF.min_eq_of_leView on Github →