Theorem Order.IsPredLimit.lt_iff_exists_lt

Modification history

2024-12-11 14:33
Mathlib/Order/SuccPred/Limit.lean
feat(Order/SuccPred/Limit): extra lemmas (#19801) …
Added Order.IsPredLimit.lt_iff_exists_ltView on Github →