Counting coding functions at base type and level zero

In this file, we show that there are less than μ coding functions at levels ⊥ and 0.

Main declarations

• ConNF.card_bot_codingFunction_lt, ConNF.card_codingFunction_lt_of_isMin: There are less than μ coding functions at levels ⊥ and 0.

theorem ConNF.card_codingFunction_lt_of_card_supportOrbit_lt [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (ν : Cardinal.{u}) (hν : ν < Cardinal.mk μ) (hβ : Cardinal.mk (SupportOrbit β) < Cardinal.mk μ) (hνS : ∀ (S : Support β), Cardinal.mk { x : TSet β // S.Supports x } ≤ ν) : Cardinal.mk (CodingFunction β) < Cardinal.mk μ

theorem ConNF.card_bot_codingFunction_lt [Params] [Level] [CoherentData] : Cardinal.mk (CodingFunction ⊥) < Cardinal.mk μ

theorem ConNF.eq_bot_of_lt_of_isMin [Params] [Level] {β : Λ} [LeLevel ↑β] (hβ : IsMin β) {δ : TypeIndex} (hδ : δ < ↑β) : δ = ⊥

theorem ConNF.allPerm_of_basePerm_of_isMin [Params] [Level] [CoherentData] {β : Λ} [LeLevel ↑β] (hβ : IsMin β) (π : BasePerm) : ∃ (ρ : AllPerm ↑β), ρᵁ (Path.nil ↘.) = π

theorem ConNF.path_eq_of_isMin [Params] [Level] {β : Λ} [LeLevel ↑β] (hβ : IsMin β) (A : ↑β ↝ ⊥) : A = Path.nil ↘.

theorem ConNF.card_codingFunction_lt_of_isMin [Params] [Level] [CoherentData] {β : Λ} [LeLevel ↑β] (hβ : IsMin β) : Cardinal.mk (CodingFunction ↑β) < Cardinal.mk μ