Theorem Finite.bddAbove_range

Modification history

2025-12-08 05:19
Mathlib/Data/Fintype/Order.lean
refactor: make `abbrev`s for `IsDirected α (· ≤ ·)` and `IsDirected α (· ≥ ·)` (#32462) …
Modified Finite.bddAbove_rangeView on Github →
2024-01-16 04:25
Mathlib/Data/Fintype/Order.lean
chore(Fintype/Order): generalize Fintype to Finite in Directed lemmas (#9754)
Added Finite.bddAbove_rangeView on Github →