def
ConNF.fuzz
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
(hβγ : β ≠ ↑γ)
:
ConNF.Tangle β → ConNF.Litter
Equations
- ConNF.fuzz hβγ = (fun (x : ConNF.μ) => { ν := x, β := β, γ := γ, β_ne_γ := hβγ }) ∘ ConNF.funOfDeny ⋯ (fun (t : ConNF.Tangle β) => {ConNF.pos t}) ⋯
Instances For
theorem
ConNF.fuzz_β_eq
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
{β' : ConNF.TypeIndex}
[ConNF.ModelData β']
[ConNF.Position (ConNF.Tangle β')]
{γ' : ConNF.Λ}
{hβγ : β ≠ ↑γ}
{hβγ' : β' ≠ ↑γ'}
{t : ConNF.Tangle β}
{t' : ConNF.Tangle β'}
(h : ConNF.fuzz hβγ t = ConNF.fuzz hβγ' t')
:
β = β'
theorem
ConNF.fuzz_γ_eq
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
{β' : ConNF.TypeIndex}
[ConNF.ModelData β']
[ConNF.Position (ConNF.Tangle β')]
{γ' : ConNF.Λ}
{hβγ : β ≠ ↑γ}
{hβγ' : β' ≠ ↑γ'}
{t : ConNF.Tangle β}
{t' : ConNF.Tangle β'}
(h : ConNF.fuzz hβγ t = ConNF.fuzz hβγ' t')
:
γ = γ'
theorem
ConNF.fuzz_injective
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
{hβγ : β ≠ ↑γ}
{t₁ t₂ : ConNF.Tangle β}
(h : ConNF.fuzz hβγ t₁ = ConNF.fuzz hβγ t₂)
:
t₁ = t₂
theorem
ConNF.fuzz_ν
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
(hβγ : β ≠ ↑γ)
(t : ConNF.Tangle β)
:
ConNF.pos t < (ConNF.fuzz hβγ t).ν
theorem
ConNF.pos_fuzz
[ConNF.Params]
{β : ConNF.TypeIndex}
[ConNF.ModelData β]
[ConNF.Position (ConNF.Tangle β)]
{γ : ConNF.Λ}
(hβγ : β ≠ ↑γ)
(t : ConNF.Tangle β)
:
ConNF.pos t < ConNF.pos (ConNF.fuzz hβγ t)