Counting coding functions #
def
ConNF.RecodeType
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(o : ConNF.SupportOrbit β)
:
Type u
Equations
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
ConNF.recodeSurjection
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
(o : ConNF.SupportOrbit β)
(x : ConNF.RecodeType hγ o)
:
Equations
- ConNF.recodeSurjection hγ o x = ConNF.raisedCodingFunction hγ (Subtype.val '' ↑x) o ⋯ ⋯
Instances For
theorem
ConNF.recodeSurjection_surjective
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
Function.Surjective fun (x : (o : ConNF.SupportOrbit β) × ConNF.RecodeType hγ o) =>
ConNF.recodeSurjection hγ x.fst x.snd
theorem
ConNF.recodeSurjection_range
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
:
Set.univ ⊆ Set.range fun (x : (o : ConNF.SupportOrbit β) × ConNF.RecodeType hγ o) => ConNF.recodeSurjection hγ x.fst x.snd
theorem
ConNF.mk_codingFunction_le
[ConNF.Params]
[ConNF.Level]
[ConNF.BasePositions]
[ConNF.CountingAssumptions]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[ConNF.LeLevel ↑β]
[ConNF.LeLevel ↑γ]
(hγ : ↑γ < ↑β)
: