New file

In this file...

Main declarations

• ConNF.foo: Something new.

structure ConNF.Motive [Params] (α : Λ) : Type (u + 1)

• data : ModelData ↑α
• pos : Position (Tangle ↑α)
• typed : TypedNearLitters α

theorem ConNF.card_tangle_bot_le [Params] [ModelData ⊥] : Cardinal.mk (Tangle ⊥) ≤ Cardinal.mk μ

def ConNF.botPosition [Params] [ModelData ⊥] : Position (Tangle ⊥)

Equations

• ConNF.botPosition = { pos := { toFun := ConNF.funOfDeny ⋯ (fun (t : ConNF.Tangle ⊥) => ⇑ConNF.pos '' (t.supportᴬ.image Prod.snd).rel.codom) ⋯, inj' := ⋯ } }

theorem ConNF.pos_tangle_bot [Params] {D : ModelData ⊥} (t : Tangle ⊥) (a : Atom) (A : ⊥ ↝ ⊥) (ha : a ∈ (t.support ⇘. A)ᴬ) : pos a < pos t

structure ConNF.Hypothesis [Params] {α : Λ} (M : Motive α) (N : (β : Λ) → ↑β < ↑α → Motive β) : Type u

• allPermSderiv {β : Λ} (h : ↑β < ↑α) : AllPerm ↑α → AllPerm ↑β
• allPermBotSderiv : AllPerm ↑α → AllPerm ⊥
• singleton {β : Λ} (h : ↑β < ↑α) : TSet ↑β → TSet ↑α
• allPermSderiv_forget {β : Λ} (h : ↑β < ↑α) (ρ : AllPerm ↑α) : PreModelData.allPermForget (self.allPermSderiv h ρ) = PreModelData.allPermForget ρ ↘ h
• allPermBotSderiv_forget (ρ : AllPerm ↑α) : PreModelData.allPermForget (self.allPermBotSderiv ρ) = PreModelData.allPermForget ρ ↘ ⋯
• pos_atom_lt_pos (t : Tangle ↑α) (A : ↑α ↝ ⊥) (a : Atom) : a ∈ (t.support ⇘. A)ᴬ → pos a < pos t
• pos_nearLitter_lt_pos (t : Tangle ↑α) (A : ↑α ↝ ⊥) (N : NearLitter) : N ∈ (t.support ⇘. A)ᴺ → pos N < pos t
• smul_fuzz {β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hβγ : ↑β ≠ ↑γ) (ρ : AllPerm ↑α) (t : Tangle ↑β) : PreModelData.allPermForget ρ ↘ hγ ↘. • fuzz hβγ t = fuzz hβγ (self.allPermSderiv hβ ρ • t)
• smul_fuzz_bot {γ : Λ} (hγ : ↑γ < ↑α) (ρ : AllPerm ↑α) (t : Tangle ⊥) : PreModelData.allPermForget ρ ↘ hγ ↘. • fuzz ⋯ t = fuzz ⋯ (self.allPermBotSderiv ρ • t)
• allPerm_of_smul_fuzz (ρs : {β : Λ} → (hβ : ↑β < ↑α) → AllPerm ↑β) (π : AllPerm ⊥) : (∀ {β γ : Λ} (hβ : ↑β < ↑α) (hγ : ↑γ < ↑α) (hδε : ↑β ≠ ↑γ) (t : Tangle ↑β), (ρs hγ)ᵁ ↘. • fuzz hδε t = fuzz hδε (ρs hβ • t)) → (∀ {γ : Λ} (hγ : ↑γ < ↑α) (t : Tangle ⊥), (ρs hγ)ᵁ ↘. • fuzz ⋯ t = fuzz ⋯ (π • t)) → ∃ (ρ : AllPerm ↑α), (∀ (β : Λ) (hβ : ↑β < ↑α), self.allPermSderiv hβ ρ = ρs hβ) ∧ self.allPermBotSderiv ρ = π
• tSet_ext (β : Λ) (hβ : ↑β < ↑α) (x y : TSet ↑α) : (∀ (z : TSet ↑β), z ∈[hβ] x ↔ z ∈[hβ] y) → x = y
• typedMem_singleton_iff {β : Λ} (hβ : ↑β < ↑α) (x y : TSet ↑β) : y ∈[hβ] self.singleton hβ x ↔ y = x

def ConNF.castTSet [Params] {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} (h₁ : α = β) (h₂ : D₁ ≍ D₂) : TSet α ≃ TSet β

Equations

• One or more equations did not get rendered due to their size.

def ConNF.castAllPerm [Params] {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} (h₁ : α = β) (h₂ : D₁ ≍ D₂) : AllPerm α ≃ AllPerm β

Equations

• One or more equations did not get rendered due to their size.

def ConNF.castTangle [Params] {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} (h₁ : α = β) (h₂ : D₁ ≍ D₂) : Tangle α ≃ Tangle β

Equations

• One or more equations did not get rendered due to their size.

theorem ConNF.castTSet_forget [Params] {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : D₁ ≍ D₂) (ρ : TSet α) : PreModelData.tSetForget ((castTSet ⋯ h₂) ρ) = PreModelData.tSetForget ρ

theorem ConNF.castAllPerm_forget [Params] {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : D₁ ≍ D₂) (ρ : AllPerm α) : PreModelData.allPermForget ((castAllPerm ⋯ h₂) ρ) = PreModelData.allPermForget ρ

theorem ConNF.castTangle_support [Params] {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : D₁ ≍ D₂) (t : Tangle α) : ((castTangle ⋯ h₂) t).support = t.support

theorem ConNF.castAllPerm_smul [Params] {α : TypeIndex} {D₁ D₂ : ModelData α} (h₂ : D₁ ≍ D₂) (ρ : AllPerm α) (t : Tangle α) : ρ • (castTangle ⋯ h₂) t = (castTangle ⋯ h₂) ((castAllPerm ⋯ h₂).symm ρ • t)

theorem ConNF.castTangle_pos [Params] {α β : TypeIndex} {D₁ : ModelData α} {D₂ : ModelData β} {E₁ : Position (Tangle α)} {E₂ : Position (Tangle β)} (h₁ : α = β) (h₂ : D₁ ≍ D₂) (h₃ : E₁ ≍ E₂) (t : Tangle α) : pos ((castTangle h₁ h₂) t) = pos t

theorem ConNF.castTangle_fuzz [Params] {α : TypeIndex} {D₁ D₂ : ModelData α} {E₁ : Position (Tangle α)} {E₂ : Position (Tangle α)} (h₂ : D₁ ≍ D₂) (h₃ : E₁ ≍ E₂) (t : Tangle α) {β : Λ} (hαβ : α ≠ ↑β) : fuzz hαβ ((castTangle ⋯ h₂) t) = fuzz hαβ t