instance ConNF.instLeLevelSomeΛOfNat [ConNF.Params] [ConNF.Level] : ConNF.LeLevel ↑0

Equations

• ⋯ = ⋯

theorem ConNF.mk_codingFunction [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] (β : ConNF.Λ) [i : ConNF.LeLevel ↑β] (hzero : Cardinal.mk (ConNF.CodingFunction 0) < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.CodingFunction β) < Cardinal.mk ConNF.μ

noncomputable def ConNF.TSet.code [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] (t : ConNF.TSet ↑β) : ConNF.CodingFunction β × ConNF.Support ↑β

Equations

• ConNF.TSet.code t = (ConNF.CodingFunction.code t.support t ⋯, t.support)

theorem ConNF.TSet.code_injective [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] {β : ConNF.Λ} [ConNF.LeLevel ↑β] : Function.Injective ConNF.TSet.code

theorem ConNF.mk_tSet [ConNF.Params] [ConNF.Level] [ConNF.BasePositions] [ConNF.CountingAssumptions] (β : ConNF.Λ) [ConNF.LeLevel ↑β] (hzero : Cardinal.mk (ConNF.CodingFunction 0) < Cardinal.mk ConNF.μ) : Cardinal.mk (ConNF.TSet ↑β) = Cardinal.mk ConNF.μ