mathlib documentation

data.pnat.intervals

source
def pnat.Ico (l u : ℕ+) :
finset ℕ+

Ico l u is the set of positive natural numbers l ≤ k < u.

Equations
source
@[simp]
theorem pnat.Ico.mem {n m l : ℕ+} :
l ∈ n.Ico m ↔ n ≤ l ∧ l < m
source
@[simp]
theorem pnat.Ico.card (l u : ℕ+) :
(l.Ico u).card = ↑u - ↑l