Commit 2026-01-30 15:11 f468b6ae

View on Github →

feat(Order/WithBot): ∀ x > ↑a, p x iff ∀ b > a, p ↑b (#34363) Upstreamed from the CGT repo.

Estimated changes

added theorem WithBot.exists_coe_le
added theorem WithBot.exists_coe_lt
added theorem WithBot.forall_coe_le
added theorem WithBot.forall_coe_lt
modified theorem WithBot.forall_ne_bot