Theorem Finset.Ici_one_eq_univ

Modification history

2026-07-01 06:16
Mathlib/Order/Interval/Finset/Defs.lean
feat(Order): `Ici (1 : α) = univ` when `IsBotOneClass α` (#40762) …
Added Finset.Ici_one_eq_univView on Github →