mathlib documentation

data.pnat.intervals

def pnat.Ico  :

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

Equations
@[simp]
theorem pnat.Ico.mem {n m l : ℕ+} :
l n.Ico m n l l < m

@[simp]
theorem pnat.Ico.card (l u : ℕ+) :
(l.Ico u).card = u - l