# Finite intervals of positive naturals #

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

theorem PNat.Icc_eq_finset_subtype (a : ℕ+) (b : ℕ+) :
= Finset.subtype (fun (n : ) => 0 < n) (Finset.Icc a b)
theorem PNat.Ico_eq_finset_subtype (a : ℕ+) (b : ℕ+) :
= Finset.subtype (fun (n : ) => 0 < n) (Finset.Ico a b)
theorem PNat.Ioc_eq_finset_subtype (a : ℕ+) (b : ℕ+) :
= Finset.subtype (fun (n : ) => 0 < n) (Finset.Ioc a b)
theorem PNat.Ioo_eq_finset_subtype (a : ℕ+) (b : ℕ+) :
= Finset.subtype (fun (n : ) => 0 < n) (Finset.Ioo a b)
theorem PNat.uIcc_eq_finset_subtype (a : ℕ+) (b : ℕ+) :
= Finset.subtype (fun (n : ) => 0 < n) (Finset.uIcc a b)
@[simp]
theorem PNat.card_Icc (a : ℕ+) (b : ℕ+) :
().card = b + 1 - a
@[simp]
theorem PNat.card_Ico (a : ℕ+) (b : ℕ+) :
().card = b - a
@[simp]
theorem PNat.card_Ioc (a : ℕ+) (b : ℕ+) :
().card = b - a
@[simp]
theorem PNat.card_Ioo (a : ℕ+) (b : ℕ+) :
().card = b - a - 1
@[simp]
theorem PNat.card_uIcc (a : ℕ+) (b : ℕ+) :
().card = (b - a).natAbs + 1
theorem PNat.card_fintype_Icc (a : ℕ+) (b : ℕ+) :
Fintype.card (Set.Icc a b) = b + 1 - a
theorem PNat.card_fintype_Ico (a : ℕ+) (b : ℕ+) :
Fintype.card (Set.Ico a b) = b - a
theorem PNat.card_fintype_Ioc (a : ℕ+) (b : ℕ+) :
Fintype.card (Set.Ioc a b) = b - a
theorem PNat.card_fintype_Ioo (a : ℕ+) (b : ℕ+) :
Fintype.card (Set.Ioo a b) = b - a - 1
theorem PNat.card_fintype_uIcc (a : ℕ+) (b : ℕ+) :
Fintype.card (Set.uIcc a b) = (b - a).natAbs + 1