Commit 2026-07-14 19:53 f98b1aa3

View on Github →

feat(Data/Fintype/Order): generalize index type to Sort* (#41714) This is helpful when dealing with biSups, as ⨆ i ∈ s, f i expands to ⨆ i, ⨆ _ : i ∈ s, f i and so sups over proofs are common.

Estimated changes

modified theorem Finite.bddAbove_range
modified theorem Finite.bddBelow_range
modified theorem Finite.exists_ge
modified theorem Finite.exists_le