mathlib documentation

data.fintype.intervals

fintype instances for intervals #

We provide fintype instances for Ico l u, for l u : ℕ, and for l u : ℤ.

@[instance]
def set.Ico_ℕ_fintype (l u : ) :
Equations
@[simp]
theorem set.Ico_ℕ_card (l u : ) :
@[instance]
Equations
@[simp]
theorem set.Ico_pnat_card (l u : ℕ+) :
@[instance]
def set.Ico_ℤ_fintype (l u : ) :
Equations
@[instance]
def set.Ioo_ℤ_fintype (l u : ) :
Equations
@[instance]
def set.Icc_ℤ_fintype (l u : ) :
Equations
@[instance]
def set.Ioc_ℤ_fintype (l u : ) :
Equations
theorem set.Ico_ℤ_finite (l u : ) :
theorem set.Ioo_ℤ_finite (l u : ) :
theorem set.Icc_ℤ_finite (l u : ) :
theorem set.Ioc_ℤ_finite (l u : ) :
@[simp]
theorem set.Ico_ℤ_card (l u : ) :
@[simp]
theorem set.Ioo_ℤ_card (l u : ) :
@[simp]
theorem set.Icc_ℤ_card (l u : ) :
@[simp]
theorem set.Ioc_ℤ_card (l u : ) :