Counting raised singletons #
theorem
ConNF.mem_orbit_of_raiseSingleton_eq
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(S₁ : ConNF.Support ↑β)
(S₂ : ConNF.Support ↑β)
(u₁ : ConNF.TSet ↑γ)
(u₂ : ConNF.TSet ↑γ)
(hS : S₁.max = S₂.max)
(hu : ConNF.CodingFunction.code u₁.support u₁ ⋯ = ConNF.CodingFunction.code u₂.support u₂ ⋯)
(hSu : ConNF.SupportOrbit.mk (ConNF.raisedSupport hγ S₁ u₁) = ConNF.SupportOrbit.mk (ConNF.raisedSupport hγ S₂ u₂))
:
ConNF.raiseSingleton hγ S₁ u₁ = ConNF.raiseSingleton hγ S₂ u₂
noncomputable def
ConNF.RaisedSingleton.code
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(r : ConNF.RaisedSingleton hγ)
:
ConNF.κ × ConNF.SupportOrbit β × ConNF.CodingFunction γ
Equations
- ConNF.RaisedSingleton.code hγ r = (⋯.choose.max, ConNF.SupportOrbit.mk (ConNF.raisedSupport hγ ⋯.choose ⋯.choose), ConNF.CodingFunction.code ⋯.choose.support ⋯.choose ⋯)
Instances For
theorem
ConNF.RaisedSingleton.code_injective
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
theorem
ConNF.mk_raisedSingleton_le
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
Cardinal.mk (ConNF.RaisedSingleton hγ) ≤ Cardinal.mk ConNF.κ * Cardinal.mk (ConNF.SupportOrbit β) * Cardinal.mk (ConNF.CodingFunction γ)