The fuzz map

In this file, we define the fuzz map.

Main declarations

• ConNF.fuzz: The fuzz map.

def ConNF.fuzz [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} (hβγ : β ≠ ↑γ) : Tangle β → Litter

Equations

• ConNF.fuzz hβγ = (fun (x : ConNF.μ) => { ν := x, β := β, γ := γ, β_ne_γ := hβγ }) ∘ ConNF.funOfDeny ⋯ (fun (t : ConNF.Tangle β) => {ConNF.pos t}) ⋯

theorem ConNF.fuzz_β_eq [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} {β' : TypeIndex} [ModelData β'] [Position (Tangle β')] {γ' : Λ} {hβγ : β ≠ ↑γ} {hβγ' : β' ≠ ↑γ'} {t : Tangle β} {t' : Tangle β'} (h : fuzz hβγ t = fuzz hβγ' t') : β = β'

theorem ConNF.fuzz_γ_eq [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} {β' : TypeIndex} [ModelData β'] [Position (Tangle β')] {γ' : Λ} {hβγ : β ≠ ↑γ} {hβγ' : β' ≠ ↑γ'} {t : Tangle β} {t' : Tangle β'} (h : fuzz hβγ t = fuzz hβγ' t') : γ = γ'

theorem ConNF.fuzz_injective [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} {hβγ : β ≠ ↑γ} {t₁ t₂ : Tangle β} (h : fuzz hβγ t₁ = fuzz hβγ t₂) : t₁ = t₂

theorem ConNF.fuzz_ν [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} (hβγ : β ≠ ↑γ) (t : Tangle β) : pos t < (fuzz hβγ t).ν

theorem ConNF.pos_fuzz [Params] {β : TypeIndex} [ModelData β] [Position (Tangle β)] {γ : Λ} (hβγ : β ≠ ↑γ) (t : Tangle β) : pos t < pos (fuzz hβγ t)