New file

In this file...

Main declarations

• ConNF.foo: Something new.

theorem ConNF.Support.not_mem_scoderiv_botDeriv [Params] {β γ : Λ} {hγ : ↑γ < ↑β} (S : Support ↑γ) (N : NearLitter) : N ∉ (S ↗ hγ ⇘. (Path.nil ↘.))ᴺ

theorem ConNF.Support.not_mem_strong_botDeriv [Params] {β γ : Λ} {hγ : ↑γ < ↑β} [Level] [LtLevel ↑β] (S : Support ↑γ) (N : NearLitter) : N ∉ ((S ↗ hγ).strong ⇘. (Path.nil ↘.))ᴺ

theorem ConNF.Support.raise_preStrong' [Params] {β γ : Λ} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ : AllPerm ↑β) (hγ : ↑γ < ↑β) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).PreStrong

theorem ConNF.Support.raise_closed' [Params] {β γ : Λ} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ : AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).Closed

theorem ConNF.Support.raise_strong' [Params] {β γ : Λ} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ : AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).Strong

theorem ConNF.Support.convAtoms_injective_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑α ↝ ⊥) : (convAtoms (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A).Injective

theorem ConNF.Support.atomMemRel_le_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑α ↝ ⊥) : atomMemRel (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A ≤ atomMemRel (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A

theorem ConNF.Support.convNearLitters_cases [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} {A : ↑α ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → N₁ = N₂ ∧ N₁ ∈ (S ⇘. A)ᴺ ∨ ∃ (B : ↑β ↝ ⊥), A = B ↗ ⋯ ∧ (ρ₁ᵁ B)⁻¹ • N₁ = (ρ₂ᵁ B)⁻¹ • N₂ ∧ (ρ₁ᵁ B)⁻¹ • N₁ ∈ (((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport) ⇘. B)ᴺ

theorem ConNF.Support.inflexible_of_inflexible_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) {A : ↑α ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (P : InflexiblePath ↑α) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → ∃ (ρ : AllPerm P.δ), N₂ᴸ = fuzz ⋯ (ρ • t)

theorem ConNF.Support.atoms_of_inflexible_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} (hS : S.Strong) {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑α ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath ↑α) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : κ), ((S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a → ((S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)

theorem ConNF.Support.nearLitters_of_inflexible_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} (hS : S.Strong) {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) (A : ↑α ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath ↑α) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : κ), ((S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N → ((S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

theorem ConNF.Support.litter_eq_of_flexible_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] {S : Support ↑α} {T : Support ↑γ} {ρ₁ ρ₂ : AllPerm ↑β} {hγ : ↑γ < ↑β} (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) {A : ↑α ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} : convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₁ N₂ → convNearLitters (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) A N₃ N₄ → ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ → N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ

theorem ConNF.Support.sameSpecLe_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ₁ ρ₂ : AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ₁ : ρ₁ᵁ • S ↘ ⋯ = S ↘ ⋯) (hρ₂ : ρ₂ᵁ • S ↘ ⋯ = S ↘ ⋯) : SameSpecLE (S + (ρ₁ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯) (S + (ρ₂ᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯)

theorem ConNF.Support.spec_same_of_fixes [Params] {β γ : Λ} {hγ : ↑γ < ↑β} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ : AllPerm ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : (S + ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport) ↗ ⋯).spec = (S + (ρᵁ • ((T ↗ hγ).strong + (S ↘ ⋯ + (T ↗ hγ).strong).interferenceSupport)) ↗ ⋯).spec

theorem ConNF.Support.exists_allowable_of_fixes [Params] {β γ : Λ} [Level] [LtLevel ↑β] (S : Support ↑α) (hS : S.Strong) (T : Support ↑γ) (ρ : AllPerm ↑β) (hγ : ↑γ < ↑β) (hρ : ρᵁ • S ↘ ⋯ = S ↘ ⋯) : ∃ (ρ' : AllPerm ↑α), ρ'ᵁ • S = S ∧ ρ'ᵁ ↘ ⋯ ↘ hγ • T = ρᵁ ↘ hγ • T