Theorem Set.PartiallyWellOrderedOn.exists_not_mem_of_gt

Modification history

2025-05-25 12:30
Mathlib/Order/WellFoundedSet.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted Set.PartiallyWellOrderedOn.exists_not_mem_of_gtView on Github →
2025-05-08 17:56
Mathlib/Order/WellFoundedSet.lean
feat (Order/WellFoundedSet): Preimage of a partially well-ordered subset along a decreasing sequence is bounded above. (#24307) …
Added Set.PartiallyWellOrderedOn.exists_not_mem_of_gtView on Github →