Theorem exists_eq_iInf_of_not_isPredPrelimit

Modification history

2026-09-07 15:38

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

chore(Order): use `to_dual` in various places (#43323) …

Deleted exists_eq_iInf_of_not_isPredPrelimit View on Github →

2024-09-06 21:42

Mathlib/Order/SuccPred/CompleteLinearOrder.lean

refactor(Order/SuccPred/Limit): `IsSuccLimit` → `IsSuccPrelimit` (#16518) …

Added exists_eq_iInf_of_not_isPredPrelimit View on Github →