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.

source
@[protected, instance]
def pnat.locally_finite_order  :
locally_finite_order ℕ+
Equations
source
theorem pnat.Icc_eq_finset_subtype (a b : ℕ+) :
finset.Icc a b = finset.subtype (λ (n : ℕ), 0 < n) (finset.Icc ↑a ↑b)
source
theorem pnat.Ico_eq_finset_subtype (a b : ℕ+) :
finset.Ico a b = finset.subtype (λ (n : ℕ), 0 < n) (finset.Ico ↑a ↑b)
source
theorem pnat.Ioc_eq_finset_subtype (a b : ℕ+) :
finset.Ioc a b = finset.subtype (λ (n : ℕ), 0 < n) (finset.Ioc ↑a ↑b)
source
theorem pnat.Ioo_eq_finset_subtype (a b : ℕ+) :
finset.Ioo a b = finset.subtype (λ (n : ℕ), 0 < n) (finset.Ioo ↑a ↑b)
source
theorem pnat.uIcc_eq_finset_subtype (a b : ℕ+) :
finset.uIcc a b = finset.subtype (λ (n : ℕ), 0 < n) (finset.uIcc ↑a ↑b)
source
theorem pnat.map_subtype_embedding_Icc (a b : ℕ+) :
finset.map (function.embedding.subtype (λ (n : ℕ), 0 < n)) (finset.Icc a b) = finset.Icc ↑a ↑b
source
theorem pnat.map_subtype_embedding_Ico (a b : ℕ+) :
finset.map (function.embedding.subtype (λ (n : ℕ), 0 < n)) (finset.Ico a b) = finset.Ico ↑a ↑b
source
theorem pnat.map_subtype_embedding_Ioc (a b : ℕ+) :
finset.map (function.embedding.subtype (λ (n : ℕ), 0 < n)) (finset.Ioc a b) = finset.Ioc ↑a ↑b
source
theorem pnat.map_subtype_embedding_Ioo (a b : ℕ+) :
finset.map (function.embedding.subtype (λ (n : ℕ), 0 < n)) (finset.Ioo a b) = finset.Ioo ↑a ↑b
source
theorem pnat.map_subtype_embedding_uIcc (a b : ℕ+) :
finset.map (function.embedding.subtype (λ (n : ℕ), 0 < n)) (finset.uIcc a b) = finset.uIcc ↑a ↑b
source
@[simp]
theorem pnat.card_Icc (a b : ℕ+) :
(finset.Icc a b).card = ↑b + 1 - ↑a
source
@[simp]
theorem pnat.card_Ico (a b : ℕ+) :
(finset.Ico a b).card = ↑b - ↑a
source
@[simp]
theorem pnat.card_Ioc (a b : ℕ+) :
(finset.Ioc a b).card = ↑b - ↑a
source
@[simp]
theorem pnat.card_Ioo (a b : ℕ+) :
(finset.Ioo a b).card = ↑b - ↑a - 1
source
@[simp]
theorem pnat.card_uIcc (a b : ℕ+) :
(finset.uIcc a b).card = (↑b - ↑a).nat_abs + 1
source
@[simp]
theorem pnat.card_fintype_Icc (a b : ℕ+) :
fintype.card ↥(set.Icc a b) = ↑b + 1 - ↑a
source
@[simp]
theorem pnat.card_fintype_Ico (a b : ℕ+) :
fintype.card ↥(set.Ico a b) = ↑b - ↑a
source
@[simp]
theorem pnat.card_fintype_Ioc (a b : ℕ+) :
fintype.card ↥(set.Ioc a b) = ↑b - ↑a
source
@[simp]
theorem pnat.card_fintype_Ioo (a b : ℕ+) :
fintype.card ↥(set.Ioo a b) = ↑b - ↑a - 1
source
@[simp]
theorem pnat.card_fintype_uIcc (a b : ℕ+) :
fintype.card ↥(set.uIcc a b) = (↑b - ↑a).nat_abs + 1