Documentation

PFR.Mathlib.Order.Interval.Finset.Defs

@[simp]
theorem Finset.Ici_one {α : Type u_1} [One α] [Preorder α] [IsBotOneClass α] [LocallyFiniteOrderTop α] [Fintype α] :
@[simp]
theorem Finset.Ici_zero {α : Type u_1} [Zero α] [Preorder α] [IsBotZeroClass α] [LocallyFiniteOrderTop α] [Fintype α] :