Theorem Set.IsWF.min_of_subset_not_lt_min

Modification history

2024-02-06 20:37
Mathlib/Order/WellFoundedSet.lean
feat: HahnSeries smul order inequality (#9848) …
Added Set.IsWF.min_of_subset_not_lt_minView on Github →