Counting coding functions at level ⊥ and 0

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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (ν : Cardinal.{u}) (hν : ν < Cardinal.mk ConNF.μ) (hβ : Cardinal.mk (ConNF.SupportOrbit β) < Cardinal.mk ConNF.μ) (hνS : ∀ (S : ConNF.Support β), Cardinal.mk { x : ConNF.TSet β // S.Supports x } ≤ ν) : Cardinal.mk (ConNF.CodingFunction β) < Cardinal.mk ConNF.μ

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

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

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

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

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