mathlib documentation

data.fintype.intervals

fintype instances for intervals #

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

@[protected, instance]

def set.Ico_ℕ_fintype (l u : ℕ) :

fintype ↥(set.Ico l u)

Equations

set.Ico_ℕ_fintype l u = fintype.of_finset (finset.Ico l u) _

@[simp]

theorem set.Ico_ℕ_card (l u : ℕ) :

fintype.card ↥(set.Ico l u) = u - l

@[protected, instance]

def set.Ico_pnat_fintype (l u : ℕ+) :

fintype ↥(set.Ico l u)

Equations

set.Ico_pnat_fintype l u = fintype.of_finset (l.Ico u) _

@[simp]

theorem set.Ico_pnat_card (l u : ℕ+) :

fintype.card ↥(set.Ico l u) = ↑u - ↑l

@[protected, instance]

def set.Ico_ℤ_fintype (l u : ℤ) :

fintype ↥(set.Ico l u)

Equations

set.Ico_ℤ_fintype l u = fintype.of_finset (finset.Ico_ℤ l u) _

@[simp]

theorem set.Ico_ℤ_card (l u : ℤ) :

fintype.card ↥(set.Ico l u) = (u - l).to_nat

theorem set.Ico_ℤ_finite (l u : ℤ) :

(set.Ico l u).finite

theorem set.Ioo_ℤ_finite (l u : ℤ) :

(set.Ioo l u).finite

theorem set.Icc_ℤ_finite (l u : ℤ) :

(set.Icc l u).finite

theorem set.Ioc_ℤ_finite (l u : ℤ) :

(set.Ioc l u).finite