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 [ConNF.Params] : Type u

• atoms : Set ConNF.κ
• nearLitters : Set ConNF.κ

structure ConNF.FlexCond [ConNF.Params] : Type u

• nearLitters : Set ConNF.κ

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

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

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

Equations

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

• ConNF.instPartialOrderSpec = PartialOrder.mk ⋯

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

Equations

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

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

Equations

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

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

Equations

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

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

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

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

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

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

theorem ConNF.nearLitterCondRel_inflex [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S : ConNF.Support β} {A : β ↝ ⊥} {N : ConNF.NearLitter} {P : ConNF.InflexiblePath β} {χ : ConNF.CodingFunction P.δ} {ta tn : ConNF.Tree (Rel ConNF.κ ConNF.κ) P.δ} : ConNF.nearLitterCondRel S A N (ConNF.NearLitterCond.inflex P { χ := χ, atoms := ta, nearLitters := tn }) → ∃ (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. ∧ Nᴸ = ConNF.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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) : (ConNF.nearLitterCondRel S A).Coinjective

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

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

Equations

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

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

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

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (S T : ConNF.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 : β ↝ ⊥), (ConNF.convAtoms S T A).OneOne
• atomMemRel_eq : ∀ (A : β ↝ ⊥), ConNF.atomMemRel S A = ConNF.atomMemRel T A
• inflexible_iff : ∀ {A : β ↝ ⊥} {N₁ N₂ : ConNF.NearLitter}, ConNF.convNearLitters S T A N₁ N₂ → ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → ((∃ (ρ : ConNF.AllPerm P.δ), N₁ᴸ = ConNF.fuzz ⋯ (ρ • t)) ↔ ∃ (ρ : ConNF.AllPerm P.δ), N₂ᴸ = ConNF.fuzz ⋯ (ρ • t))
• litter_eq_iff_of_flexible : ∀ {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : ConNF.NearLitter}, ConNF.convNearLitters S T A N₁ N₂ → ConNF.convNearLitters S T A N₃ N₄ → ¬ConNF.Inflexible A N₁ᴸ → ¬ConNF.Inflexible A N₂ᴸ → ¬ConNF.Inflexible A N₃ᴸ → ¬ConNF.Inflexible A N₄ᴸ → (N₁ᴸ = N₃ᴸ ↔ N₂ᴸ = N₄ᴸ)
• atoms_iff_of_inflexible : ∀ (A : β ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : ConNF.κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a ↔ (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)
• nearLitters_iff_of_inflexible : ∀ (A : β ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : ConNF.κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N ↔ (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

structure ConNF.SameSpecLE [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] (S T : ConNF.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 : β ↝ ⊥), (ConNF.convAtoms S T A).Injective
• atomMemRel_le : ∀ (A : β ↝ ⊥), ConNF.atomMemRel S A ≤ ConNF.atomMemRel T A
• inflexible_of_inflexible : ∀ {A : β ↝ ⊥} {N₁ N₂ : ConNF.NearLitter}, ConNF.convNearLitters S T A N₁ N₂ → ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → ∃ (ρ : ConNF.AllPerm P.δ), N₂ᴸ = ConNF.fuzz ⋯ (ρ • t)
• litter_eq_of_flexible : ∀ {A : β ↝ ⊥} {N₁ N₂ N₃ N₄ : ConNF.NearLitter}, ConNF.convNearLitters S T A N₁ N₂ → ConNF.convNearLitters S T A N₃ N₄ → ¬ConNF.Inflexible A N₁ᴸ → ¬ConNF.Inflexible A N₂ᴸ → ¬ConNF.Inflexible A N₃ᴸ → ¬ConNF.Inflexible A N₄ᴸ → N₁ᴸ = N₃ᴸ → N₂ᴸ = N₄ᴸ
• atoms_of_inflexible : ∀ (A : β ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ a ∈ (t.support ⇘. B)ᴬ, ∀ (i : ConNF.κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i a → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴬ.rel i (ρᵁ B • a)
• nearLitters_of_inflexible : ∀ (A : β ↝ ⊥) (N₁ N₂ : ConNF.NearLitter) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ), A = P.A ↘ ⋯ ↘. → N₁ᴸ = ConNF.fuzz ⋯ t → N₂ᴸ = ConNF.fuzz ⋯ (ρ • t) → ConNF.convNearLitters S T A N₁ N₂ → ∀ (B : P.δ ↝ ⊥), ∀ N ∈ (t.support ⇘. B)ᴺ, ∀ (i : ConNF.κ), (S ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i N → (T ⇘. (P.A ↘ ⋯ ⇘ B))ᴺ.rel i (ρᵁ B • N)

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

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

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

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

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

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

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

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

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

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

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

theorem ConNF.Support.atoms_dom_subset_of_spec_eq_spec [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S T : ConNF.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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S T : ConNF.Support β} (h : S.spec = T.spec) (A : β ↝ ⊥) : (S ⇘. A)ᴺ.rel.dom ⊆ (T ⇘. A)ᴺ.rel.dom

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

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

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

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

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

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

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

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

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

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

theorem ConNF.Support.nearLitterCondRelInflex_of_convNearLitters [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S T : ConNF.Support β} (h : ConNF.SameSpec S T) {A : β ↝ ⊥} {N₁ N₂ : ConNF.NearLitter} (hN : ConNF.convNearLitters S T A N₁ N₂) (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (ρ : ConNF.AllPerm P.δ) (hA : A = P.A ↘ ⋯ ↘.) (hN₁ : N₁ᴸ = ConNF.fuzz ⋯ t) (hN₂ : N₂ᴸ = ConNF.fuzz ⋯ (ρ • t)) : ConNF.nearLitterCondRelInflex T A N₂ (ConNF.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 [ConNF.Params] [ConNF.Level] [ConNF.CoherentData] {β : ConNF.TypeIndex} [ConNF.LeLevel β] {S T : ConNF.Support β} (h : ConNF.SameSpec S T) : S.spec ≤ T.spec

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