# mathlib3documentation

data.pnat.interval

# Finite intervals of positive naturals #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves that ℕ+ is a locally_finite_order and calculates the cardinality of its intervals as finsets and fintypes.

@[protected, instance]
Equations
theorem pnat.Icc_eq_finset_subtype (a b : ℕ+) :
b = finset.subtype (λ (n : ), 0 < n) b)
theorem pnat.Ico_eq_finset_subtype (a b : ℕ+) :
b = finset.subtype (λ (n : ), 0 < n) b)
theorem pnat.Ioc_eq_finset_subtype (a b : ℕ+) :
b = finset.subtype (λ (n : ), 0 < n) b)
theorem pnat.Ioo_eq_finset_subtype (a b : ℕ+) :
b = finset.subtype (λ (n : ), 0 < n) b)
theorem pnat.uIcc_eq_finset_subtype (a b : ℕ+) :
b = finset.subtype (λ (n : ), 0 < n) b)
@[simp]
theorem pnat.card_Icc (a b : ℕ+) :
b).card = b + 1 - a
@[simp]
theorem pnat.card_Ico (a b : ℕ+) :
b).card = b - a
@[simp]
theorem pnat.card_Ioc (a b : ℕ+) :
b).card = b - a
@[simp]
theorem pnat.card_Ioo (a b : ℕ+) :
b).card = b - a - 1
@[simp]
theorem pnat.card_uIcc (a b : ℕ+) :
b).card = (b - a).nat_abs + 1
@[simp]
theorem pnat.card_fintype_Icc (a b : ℕ+) :
@[simp]
@[simp]
@[simp]
theorem pnat.card_fintype_Ioo (a b : ℕ+) :
@[simp]