Theorem Set.unbounded_ge_of_forall_exists_gt

Modification history

2026-09-07 15:38
Mathlib/Order/Bounded.lean
chore(Order): use `to_dual` in various places (#43323) …
Deleted Set.unbounded_ge_of_forall_exists_gtView on Github →
2022-12-16 03:25
Mathlib/Order/Bounded.lean
feat: port Order.Bounded (#1042) …
Added Set.unbounded_ge_of_forall_exists_gtView on Github →