mathlib3 documentation

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.

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