Theorem WithBot.exists_coe_le

Modification history

2026-01-30 15:11
Mathlib/Order/WithBot.lean
feat(Order/WithBot): `∀ x > ↑a, p x` iff `∀ b > a, p ↑b` (#34363) …
Added WithBot.exists_coe_leView on Github →