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 : ℕ) :

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

@[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

@[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