Theorem WithBot.forall_ne_bot

Modification history

2026-01-30 15:11
Mathlib/Order/WithBot.lean
feat(Order/WithBot): `∀ x > ↑a, p x` iff `∀ b > a, p ↑b` (#34363) …
Modified WithBot.forall_ne_botView on Github →
2025-10-05 07:59
Mathlib/Order/WithBot.lean
feat: {forall,exists}_ne_{top,bot} (#30208) …
Added WithBot.forall_ne_botView on Github →