Documentation

Mathlib.Data.PNat.Interval

Finite intervals of positive naturals #

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

source
instance PNat.instLocallyFiniteOrder :
LocallyFiniteOrder ℕ+
Equations
    source
    theorem PNat.Icc_eq_finset_subtype (a b : ℕ+) :
    Finset.Icc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Icc ↑a ↑b)
    source
    theorem PNat.Ico_eq_finset_subtype (a b : ℕ+) :
    Finset.Ico a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ico ↑a ↑b)
    source
    theorem PNat.Ioc_eq_finset_subtype (a b : ℕ+) :
    Finset.Ioc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ioc ↑a ↑b)
    source
    theorem PNat.Ioo_eq_finset_subtype (a b : ℕ+) :
    Finset.Ioo a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.Ioo ↑a ↑b)
    source
    theorem PNat.uIcc_eq_finset_subtype (a b : ℕ+) :
    Finset.uIcc a b = Finset.subtype (fun (n : ℕ) => 0 < n) (Finset.uIcc ↑a ↑b)
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    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).natAbs + 1
    source
    theorem PNat.card_fintype_Icc (a b : ℕ+) :
    Fintype.card ↑(Set.Icc a b) = ↑b + 1 - ↑a
    source
    theorem PNat.card_fintype_Ico (a b : ℕ+) :
    Fintype.card ↑(Set.Ico a b) = ↑b - ↑a
    source
    theorem PNat.card_fintype_Ioc (a b : ℕ+) :
    Fintype.card ↑(Set.Ioc a b) = ↑b - ↑a
    source
    theorem PNat.card_fintype_Ioo (a b : ℕ+) :
    Fintype.card ↑(Set.Ioo a b) = ↑b - ↑a - 1
    source
    theorem PNat.card_fintype_uIcc (a b : ℕ+) :
    Fintype.card ↑(Set.uIcc a b) = (↑↑b - ↑↑a).natAbs + 1