Finite intervals of positive naturals

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

instance instLocallyFiniteOrderPNatToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeInstPNatLinearOrder : LocallyFiniteOrder ℕ+

Equations

• instLocallyFiniteOrderPNatToPreorderToPartialOrderToSemilatticeInfToLatticeInstDistribLatticeInstPNatLinearOrder = Subtype.instLocallyFiniteOrder fun (n : ℕ) => 0 < n

theorem PNat.Icc_eq_finset_subtype (a : ℕ+) (b : ℕ+) : Finset.Icc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Icc ↑a ↑b)

theorem PNat.Ico_eq_finset_subtype (a : ℕ+) (b : ℕ+) : Finset.Ico a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ico ↑a ↑b)

theorem PNat.Ioc_eq_finset_subtype (a : ℕ+) (b : ℕ+) : Finset.Ioc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ioc ↑a ↑b)

theorem PNat.Ioo_eq_finset_subtype (a : ℕ+) (b : ℕ+) : Finset.Ioo a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ioo ↑a ↑b)

theorem PNat.uIcc_eq_finset_subtype (a : ℕ+) (b : ℕ+) : Finset.uIcc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.uIcc ↑a ↑b)

theorem PNat.map_subtype_embedding_Icc (a : ℕ+) (b : ℕ+) : Finset.map (Function.Embedding.subtype fun (n : ℕ) => 0 < n) (Finset.Icc a b) = Finset.Icc ↑a ↑b

theorem PNat.map_subtype_embedding_Ico (a : ℕ+) (b : ℕ+) : Finset.map (Function.Embedding.subtype fun (n : ℕ) => 0 < n) (Finset.Ico a b) = Finset.Ico ↑a ↑b

theorem PNat.map_subtype_embedding_Ioc (a : ℕ+) (b : ℕ+) : Finset.map (Function.Embedding.subtype fun (n : ℕ) => 0 < n) (Finset.Ioc a b) = Finset.Ioc ↑a ↑b

theorem PNat.map_subtype_embedding_Ioo (a : ℕ+) (b : ℕ+) : Finset.map (Function.Embedding.subtype fun (n : ℕ) => 0 < n) (Finset.Ioo a b) = Finset.Ioo ↑a ↑b

theorem PNat.map_subtype_embedding_uIcc (a : ℕ+) (b : ℕ+) : Finset.map (Function.Embedding.subtype fun (n : ℕ) => 0 < n) (Finset.uIcc a b) = Finset.uIcc ↑a ↑b

@[simp]

theorem PNat.card_Icc (a : ℕ+) (b : ℕ+) : (Finset.Icc a b).card = ↑b + 1 - ↑a

@[simp]

theorem PNat.card_Ico (a : ℕ+) (b : ℕ+) : (Finset.Ico a b).card = ↑b - ↑a

@[simp]

theorem PNat.card_Ioc (a : ℕ+) (b : ℕ+) : (Finset.Ioc a b).card = ↑b - ↑a

@[simp]

theorem PNat.card_Ioo (a : ℕ+) (b : ℕ+) : (Finset.Ioo a b).card = ↑b - ↑a - 1

@[simp]

theorem PNat.card_uIcc (a : ℕ+) (b : ℕ+) : (Finset.uIcc a b).card = Int.natAbs (↑↑b - ↑↑a) + 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) = Int.natAbs (↑↑b - ↑↑a) + 1