Specifications for supports

In this file, we define the notion of a specification for a support.

Main declarations

• ConNF.Spec: Specifications for supports.

structure ConNF.AtomCond [Params] : Type u

• atoms : Set κ
• nearLitters : Set κ

structure ConNF.FlexCond [Params] : Type u

• nearLitters : Set κ

structure ConNF.InflexCond [Params] [Level] [CoherentData] (δ : TypeIndex) [LeLevel δ] : Type u

• χ : CodingFunction δ
• atoms : Tree (Rel κ κ) δ
• nearLitters : Tree (Rel κ κ) δ

instance ConNF.instSuperAInflexCondTreeRelκ [Params] [Level] [CoherentData] (δ : TypeIndex) [LeLevel δ] : SuperA (InflexCond δ) (Tree (Rel κ κ) δ)

Equations

• ConNF.instSuperAInflexCondTreeRelκ δ = { superA := ConNF.InflexCond.atoms }

instance ConNF.instSuperNInflexCondTreeRelκ [Params] [Level] [CoherentData] (δ : TypeIndex) [LeLevel δ] : SuperN (InflexCond δ) (Tree (Rel κ κ) δ)

Equations

• ConNF.instSuperNInflexCondTreeRelκ δ = { superN := ConNF.InflexCond.nearLitters }

inductive ConNF.NearLitterCond [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Type u

• flex [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : FlexCond → NearLitterCond β
• inflex [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (P : InflexiblePath β) : InflexCond P.δ → NearLitterCond β

structure ConNF.Spec [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : Type u

• atoms : Tree (Enumeration AtomCond) β
• nearLitters : Tree (Enumeration (NearLitterCond β)) β

instance ConNF.instSuperASpecTreeEnumerationAtomCond [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : SuperA (Spec β) (Tree (Enumeration AtomCond) β)

Equations

• ConNF.instSuperASpecTreeEnumerationAtomCond β = { superA := ConNF.Spec.atoms }

instance ConNF.instSuperNSpecTreeEnumerationNearLitterCond [Params] [Level] [CoherentData] (β : TypeIndex) [LeLevel β] : SuperN (Spec β) (Tree (Enumeration (NearLitterCond β)) β)

Equations

• ConNF.instSuperNSpecTreeEnumerationNearLitterCond β = { superN := ConNF.Spec.nearLitters }

theorem ConNF.Spec.ext [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {σ τ : Spec β} (h₁ : ∀ (A : β ↝ ⊥), σᴬ A = τᴬ A) (h₂ : ∀ (A : β ↝ ⊥), σᴺ A = τᴺ A) : σ = τ

instance ConNF.instLESpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : LE (Spec β)

Equations

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

instance ConNF.instPartialOrderSpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] : PartialOrder (Spec β)

Equations

• ConNF.instPartialOrderSpec = PartialOrder.mk ⋯

def ConNF.nearLitterCondRelFlex [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : Rel NearLitter (NearLitterCond β)

Equations

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

def ConNF.nearLitterCondRelInflex [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : Rel NearLitter (NearLitterCond β)

Equations

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

def ConNF.nearLitterCondRel [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : Rel NearLitter (NearLitterCond β)

Equations

• ConNF.nearLitterCondRel S A = ConNF.nearLitterCondRelFlex S A ⊔ ConNF.nearLitterCondRelInflex S A

theorem ConNF.nearLitterCondRelFlex_coinjective [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} : (nearLitterCondRelFlex S A).Coinjective

theorem ConNF.nearLitterCondRelInflex_coinjective [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} : (nearLitterCondRelInflex S A).Coinjective

theorem ConNF.flexible_of_mem_dom_nearLitterCondFlexRel [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} {N : NearLitter} (h : N ∈ (nearLitterCondRelFlex S A).dom) : ¬Inflexible A Nᴸ

theorem ConNF.inflexible_of_mem_dom_nearLitterCondInflexRel [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} {N : NearLitter} (h : N ∈ (nearLitterCondRelInflex S A).dom) : Inflexible A Nᴸ

theorem ConNF.nearLitterCondRel_dom_disjoint [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} : Disjoint (nearLitterCondRelFlex S A).dom (nearLitterCondRelInflex S A).dom

theorem ConNF.nearLitterCondRel_inflex [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S : Support β} {A : β ↝ ⊥} {N : NearLitter} {P : InflexiblePath β} {χ : CodingFunction P.δ} {ta tn : Tree (Rel κ κ) P.δ} : nearLitterCondRel S A N (NearLitterCond.inflex P { χ := χ, atoms := ta, nearLitters := tn }) → ∃ (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ Nᴸ = fuzz ⋯ t ∧ χ = t.code ∧ (ta = fun (B : P.δ ↝ ⊥) => (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel.comp (t.support ⇘. B)ᴬ.rel.inv) ∧ tn = fun (B : P.δ ↝ ⊥) => (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel.comp (t.support ⇘. B)ᴺ.rel.inv

theorem ConNF.nearLitterCondRel_coinjective [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (nearLitterCondRel S A).Coinjective

theorem ConNF.nearLitterCondRel_cosurjective [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (nearLitterCondRel S A).Cosurjective

def ConNF.Support.spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) : Spec β

Equations

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

theorem ConNF.Support.spec_atoms [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : S.specᴬ A = (S ⇘. A)ᴬ.image fun (a : Atom) => { atoms := {i : κ | (S ⇘. A)ᴬ.rel i a}, nearLitters := {i : κ | ∃ (N : NearLitter), (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ} }

theorem ConNF.Support.spec_nearLitters [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : S.specᴺ A = (S ⇘. A)ᴺ.comp (nearLitterCondRel S A) ⋯

theorem ConNF.Support.spec_atoms_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.specᴬ A).rel.dom = (S ⇘. A)ᴬ.rel.dom

theorem ConNF.Support.spec_nearLitters_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S : Support β) (A : β ↝ ⊥) : (S.specᴺ A).rel.dom = (S ⇘. A)ᴺ.rel.dom

def ConNF.convAtoms [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : Rel Atom Atom

Equations

• ConNF.convAtoms S T A = (S ⇘. A)ᴬ.rel.inv.comp (T ⇘. A)ᴬ.rel

def ConNF.convNearLitters [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : Rel NearLitter NearLitter

Equations

• ConNF.convNearLitters S T A = (S ⇘. A)ᴺ.rel.inv.comp (T ⇘. A)ᴺ.rel

@[simp]

theorem ConNF.convAtoms_inv [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : (convAtoms S T A).inv = convAtoms T S A

@[simp]

theorem ConNF.convNearLitters_inv [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : (convNearLitters S T A).inv = convNearLitters T S A

theorem ConNF.convAtoms_dom_subset [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : (convAtoms S T A).dom ⊆ (S ⇘. A)ᴬ.rel.codom

theorem ConNF.convNearLitters_dom_subset [Params] {β : TypeIndex} (S T : Support β) (A : β ↝ ⊥) : (convNearLitters S T A).dom ⊆ (S ⇘. A)ᴺ.rel.codom

def ConNF.atomMemRel [Params] {β : TypeIndex} (S : Support β) (A : β ↝ ⊥) : Rel κ κ

Equations

• ConNF.atomMemRel S A = (S ⇘. A)ᴺ.rel.comp (Rel.comp (fun (N : ConNF.NearLitter) (a : ConNF.Atom) => a ∈ Nᴬ) (S ⇘. A)ᴬ.rel.inv)

structure ConNF.SameSpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S T : Support β) : Prop

• atoms_bound_eq (A : β ↝ ⊥) : (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound
• nearLitters_bound_eq (A : β ↝ ⊥) : (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound
• atoms_dom_eq (A : β ↝ ⊥) : (S ⇘. A)ᴬ.rel.dom = (T ⇘. A)ᴬ.rel.dom
• nearLitters_dom_eq (A : β ↝ ⊥) : (S ⇘. A)ᴺ.rel.dom = (T ⇘. A)ᴺ.rel.dom
• convAtoms_oneOne (A : β ↝ ⊥) : (convAtoms S T A).OneOne
• atomMemRel_eq (A : β ↝ ⊥) : atomMemRel S A = atomMemRel T A
• inflexible_iff {A : β ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters S T A N₁ N₂ → ∀ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. → ((∃ (ρ : AllPerm P.δ), N₁ᴸ = fuzz ⋯ (ρ • t)) ↔ ∃ (ρ : AllPerm P.δ), N₂ᴸ = fuzz ⋯ (ρ • t))
• litter_eq_iff_of_flexible {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} : convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ → ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ → (N₁ᴸ = N₃ᴸ ↔ N₂ᴸ = N₄ᴸ)
• atoms_iff_of_inflexible (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a ↔ (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)
• nearLitters_iff_of_inflexible (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N ↔ (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

structure ConNF.SameSpecLE [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S T : Support β) : Prop

A variant of SameSpec in which most equalities have been turned into one-directional implications. It can sometimes be easier to prove this in generality than to prove SameSpec directly.

• atoms_bound_eq (A : β ↝ ⊥) : (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound
• nearLitters_bound_eq (A : β ↝ ⊥) : (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound
• atoms_dom_subset (A : β ↝ ⊥) : (S ⇘. A)ᴬ.rel.dom ⊆ (T ⇘. A)ᴬ.rel.dom
• nearLitters_dom_subset (A : β ↝ ⊥) : (S ⇘. A)ᴺ.rel.dom ⊆ (T ⇘. A)ᴺ.rel.dom
• convAtoms_injective (A : β ↝ ⊥) : (convAtoms S T A).Injective
• atomMemRel_le (A : β ↝ ⊥) : atomMemRel S A ≤ atomMemRel T A
• inflexible_of_inflexible {A : β ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters S T A N₁ N₂ → ∀ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → ∃ (ρ : AllPerm P.δ), N₂ᴸ = fuzz ⋯ (ρ • t)
• litter_eq_of_flexible {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} : convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ → ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ → N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ
• atoms_of_inflexible (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)
• nearLitters_of_inflexible (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

theorem ConNF.SameSpec.atoms_dom_of_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {i : κ} {a : Atom} (ha : (S ⇘. A)ᴬ.rel i a) : ∃ (b : Atom), (T ⇘. A)ᴬ.rel i b

theorem ConNF.SameSpec.nearLitters_dom_of_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {i : κ} {N₁ : NearLitter} (hN₁ : (S ⇘. A)ᴺ.rel i N₁) : ∃ (N₂ : NearLitter), (T ⇘. A)ᴺ.rel i N₂

theorem ConNF.SameSpec.inflexible_iff' [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (h' : convNearLitters S T A N₁ N₂) : Inflexible A N₁ᴸ ↔ Inflexible A N₂ᴸ

theorem ConNF.sameSpec_antisymm [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h₁ : SameSpecLE S T) (h₂ : SameSpecLE T S) : SameSpec S T

theorem ConNF.sameSpec_comm [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) : SameSpec T S

theorem ConNF.Support.atoms_eq_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : ((S ⇘. A)ᴬ.image fun (a : Atom) => { atoms := {i : κ | (S ⇘. A)ᴬ.rel i a}, nearLitters := {i : κ | ∃ (N : NearLitter), (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ} }) = (T ⇘. A)ᴬ.image fun (a : Atom) => { atoms := {i : κ | (T ⇘. A)ᴬ.rel i a}, nearLitters := {i : κ | ∃ (N : NearLitter), (T ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ} }

theorem ConNF.Support.nearLitters_eq_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴺ.comp (nearLitterCondRel S A) ⋯ = (T ⇘. A)ᴺ.comp (nearLitterCondRel T A) ⋯

theorem ConNF.Support.convAtoms_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) {A : β ↝ ⊥} {a b : Atom} : convAtoms S T A a b → (∀ (i : κ), (S ⇘. A)ᴬ.rel i a ↔ (T ⇘. A)ᴬ.rel i b) ∧ ∀ (i : κ), (∃ (N : NearLitter), (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ) ↔ ∃ (N : NearLitter), (T ⇘. A)ᴺ.rel i N ∧ b ∈ Nᴬ

theorem ConNF.Support.convNearLitters_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters S T A N₁ N₂ → ∃ (c : NearLitterCond β), nearLitterCondRel S A N₁ c ∧ nearLitterCondRel T A N₂ c

theorem ConNF.Support.atoms_bound_eq_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴬ.bound = (T ⇘. A)ᴬ.bound

theorem ConNF.Support.nearLitters_bound_eq_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴺ.bound = (T ⇘. A)ᴺ.bound

theorem ConNF.Support.atoms_dom_subset_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴬ.rel.dom ⊆ (T ⇘. A)ᴬ.rel.dom

theorem ConNF.Support.nearLitters_dom_subset_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴺ.rel.dom ⊆ (T ⇘. A)ᴺ.rel.dom

theorem ConNF.Support.convAtoms_injective_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (convAtoms S T A).Injective

theorem ConNF.Support.atomMemRel_le_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : atomMemRel S A ≤ atomMemRel T A

theorem ConNF.Support.inflexible_of_inflexible_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} : convNearLitters S T A N₁ N₂ → ∀ (P : InflexiblePath β) (t : Tangle P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → ∃ (ρ : AllPerm P.δ), N₂ᴸ = fuzz ⋯ (ρ • t)

theorem ConNF.Support.litter_eq_of_flexible_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : NearLitter} : convNearLitters S T A N₁ N₂ → convNearLitters S T A N₃ N₄ → ¬Inflexible A N₁ᴸ → ¬Inflexible A N₂ᴸ → ¬Inflexible A N₃ᴸ → ¬Inflexible A N₄ᴸ → N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ

theorem ConNF.Support.atoms_of_inflexible_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)

theorem ConNF.Support.nearLitters_of_inflexible_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) (N₁ N₂ : NearLitter) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) : A = P.A ↘ ⋯ ↘. → N₁ᴸ = fuzz ⋯ t → N₂ᴸ = fuzz ⋯ (ρ • t) → convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

theorem ConNF.Support.sameSpecLe_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : S.spec = T.spec) : SameSpecLE S T

theorem ConNF.Support.atoms_subset_of_sameSpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {i : κ} {a b : Atom} (ha : (S ⇘. A)ᴬ.rel i a) (hb : (T ⇘. A)ᴬ.rel i b) : {i : κ | (T ⇘. A)ᴬ.rel i b} ⊆ {i : κ | (S ⇘. A)ᴬ.rel i a}

theorem ConNF.Support.nearLitters_subset_of_sameSpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {i : κ} {a b : Atom} (ha : (S ⇘. A)ᴬ.rel i a) (hb : (T ⇘. A)ᴬ.rel i b) : {i : κ | ∃ (N : NearLitter), (T ⇘. A)ᴺ.rel i N ∧ b ∈ Nᴬ} ⊆ {i : κ | ∃ (N : NearLitter), (S ⇘. A)ᴺ.rel i N ∧ a ∈ Nᴬ}

theorem ConNF.Support.nearLitterCondRelFlex_of_convNearLitters_aux [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (hN : convNearLitters S T A N₁ N₂) (hN₁i : ¬Inflexible A N₁ᴸ) (hN₂i : ¬Inflexible A N₂ᴸ) (i : κ) : (∃ (N₃ : NearLitter), (S ⇘. A)ᴺ.rel i N₃ ∧ N₁ᴸ = N₃ᴸ) → ∃ (N₃ : NearLitter), (T ⇘. A)ᴺ.rel i N₃ ∧ N₂ᴸ = N₃ᴸ

theorem ConNF.Support.nearLitterCondRelFlex_of_convNearLitters [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (hN : convNearLitters S T A N₁ N₂) (hN₁i : ¬Inflexible A N₁ᴸ) (hN₂i : ¬Inflexible A N₂ᴸ) : nearLitterCondRelFlex T A N₂ (NearLitterCond.flex { nearLitters := {i : κ | ∃ (N₃ : NearLitter), (S ⇘. A)ᴺ.rel i N₃ ∧ N₁ᴸ = N₃ᴸ} })

theorem ConNF.Support.nearLitterCondRelInflex_of_convNearLitters [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (hN : convNearLitters S T A N₁ N₂) (P : InflexiblePath β) (t : Tangle P.δ) (ρ : AllPerm P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = fuzz ⋯ t) (hN₂ : N₂ᴸ = fuzz ⋯ (ρ • t)) : nearLitterCondRelInflex T A N₂ (NearLitterCond.inflex P { χ := t.code, atoms := fun (B : P.δ ↝ ⊥) => (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel.comp (t.support ⇘. B)ᴬ.rel.inv, nearLitters := fun (B : P.δ ↝ ⊥) => (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel.comp (t.support ⇘. B)ᴺ.rel.inv })

theorem ConNF.Support.spec_le_spec_of_sameSpec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (h : SameSpec S T) : S.spec ≤ T.spec

theorem ConNF.Support.spec_eq_spec_iff [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] (S T : Support β) : S.spec = T.spec ↔ SameSpec S T