Theorem Set.PartiallyWellOrderedOn.bddAbove_preimage

Modification history

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.bddAbove_preimageView on Github →