Strong supports

In this file, we define strong supports.

Main declarations

• ConNF.Support.Strong: The property that a support is strong.

structure ConNF.BaseSupport.Closed [ConNF.Params] (S : ConNF.BaseSupport) : Prop

• interference_subset : ∀ {N₁ N₂ : ConNF.NearLitter}, N₁ ∈ Sᴺ → N₂ ∈ Sᴺ → ∀ a ∈ ConNF.interference N₁ N₂, a ∈ Sᴬ

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

• support_le : ∀ {A : β ↝ ⊥} {N : ConNF.NearLitter}, N ∈ (S ⇘. A)ᴺ → ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → Nᴸ = ConNF.fuzz ⋯ t → t.support ≤ S ⇘ (P.A ↘ ⋯)

structure ConNF.Support.Closed [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : Prop

• closed : ∀ (A : β ↝ ⊥), (S ⇘. A).Closed

structure ConNF.Support.Strong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) extends S.PreStrong, S.Closed : Prop

• support_le : ∀ {A : β ↝ ⊥} {N : ConNF.NearLitter}, N ∈ (S ⇘. A)ᴺ → ∀ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ), A = P.A ↘ ⋯ ↘. → Nᴸ = ConNF.fuzz ⋯ t → t.support ≤ S ⇘ (P.A ↘ ⋯)
• closed : ∀ (A : β ↝ ⊥), (S ⇘. A).Closed

theorem ConNF.Support.PreStrong.smul [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {S : ConNF.Support β} (hS : S.PreStrong) (ρ : ConNF.AllPerm β) : (ρᵁ • S).PreStrong

theorem ConNF.Support.Closed.smul [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {S : ConNF.Support β} (hS : S.Closed) (ρ : ConNF.AllPerm β) : (ρᵁ • S).Closed

theorem ConNF.Support.Strong.smul [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {S : ConNF.Support β} (hS : S.Strong) (ρ : ConNF.AllPerm β) : (ρᵁ • S).Strong

theorem ConNF.Support.PreStrong.add [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {S T : ConNF.Support β} (hS : S.PreStrong) (hT : T.PreStrong) : (S + T).PreStrong

theorem ConNF.Support.Closed.scoderiv [ConNF.Params] {β γ : ConNF.TypeIndex} {S : ConNF.Support γ} (hS : S.Closed) (hγ : γ < β) : (S ↗ hγ).Closed

def ConNF.Support.Constrains [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] : Rel (β ↝ ⊥ × ConNF.NearLitter) (β ↝ ⊥ × ConNF.NearLitter)

Equations

• ConNF.Support.Constrains x y = ∃ (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (B : P.δ ↝ ⊥), x.1 = P.A ↘ ⋯ ⇘ B ∧ x.2 ∈ (t.support ⇘. B)ᴺ ∧ y.1 = P.A ↘ ⋯ ↘. ∧ y.2ᴸ = ConNF.fuzz ⋯ t

theorem ConNF.Support.constrains_subrelation [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] : Subrelation ConNF.Support.Constrains (InvImage (fun (x1 x2 : ConNF.NearLitter) => ConNF.pos x1 < ConNF.pos x2) Prod.snd)

theorem ConNF.Support.constrains_wf [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] : WellFounded ConNF.Support.Constrains

theorem ConNF.Support.not_constrains_of_flexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {x : β ↝ ⊥ × ConNF.NearLitter} {A : β ↝ ⊥} {N : ConNF.NearLitter} (h : ¬ConNF.Inflexible A Nᴸ) : ¬ConNF.Support.Constrains x (A, N)

theorem ConNF.Support.constrains_iff_of_inflexible [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] {x : β ↝ ⊥ × ConNF.NearLitter} {A : β ↝ ⊥} {N : ConNF.NearLitter} (P : ConNF.InflexiblePath β) (t : ConNF.Tangle P.δ) (hA : A = P.A ↘ ⋯ ↘.) (ht : Nᴸ = ConNF.fuzz ⋯ t) : ConNF.Support.Constrains x (A, N) ↔ x ∈ (t.support ⇗ (P.A ↘ ⋯))ᴺ

theorem ConNF.Support.constrains_small [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (y : β ↝ ⊥ × ConNF.NearLitter) : ConNF.Small {x : β ↝ ⊥ × ConNF.NearLitter | ConNF.Support.Constrains x y}

theorem ConNF.Support.reflTransGen_constrains_small [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (s : Set (β ↝ ⊥ × ConNF.NearLitter)) (hs : ConNF.Small s) : ConNF.Small {x : β ↝ ⊥ × ConNF.NearLitter | ∃ y ∈ s, Relation.ReflTransGen ConNF.Support.Constrains x y}

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

A support that contains all of the near-litters that transitively constrain something in S.

Equations

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

theorem ConNF.Support.mem_constrainsNearLitters_nearLitters [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) (N : ConNF.NearLitter) : N ∈ (S.constrainsNearLitters ⇘. A)ᴺ ↔ ∃ (B : β ↝ ⊥), ∃ N' ∈ (S ⇘. B)ᴺ, Relation.ReflTransGen ConNF.Support.Constrains (A, N) (B, N')

theorem ConNF.Support.constrainsNearLitters_atoms [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) : (S.constrainsNearLitters ⇘. A)ᴬ = ConNF.Enumeration.empty

def ConNF.Support.ConstrainsAtom [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (a : β ↝ ⊥ × ConNF.Atom) : Prop

Equations

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

theorem ConNF.Support.constrainsAtoms_small [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : ConNF.Small {a : β ↝ ⊥ × ConNF.Atom | S.ConstrainsAtom a}

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

A support that contains all the atoms that constrain something in S.

Equations

• S.constrainsAtoms = { atoms := ConNF.Enumeration.ofSet {a : β ↝ ⊥ × ConNF.Atom | S.ConstrainsAtom a} ⋯, nearLitters := ConNF.Enumeration.empty }

theorem ConNF.Support.mem_constrainsAtoms_atoms [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) (a : ConNF.Atom) : a ∈ (S.constrainsAtoms ⇘. A)ᴬ ↔ S.ConstrainsAtom (A, a)

theorem ConNF.Support.constrainsAtoms_nearLitters [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) : (S.constrainsAtoms ⇘. A)ᴺ = ConNF.Enumeration.empty

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

Equations

• S.preStrong = S + S.constrainsNearLitters + (S + S.constrainsNearLitters).constrainsAtoms

theorem ConNF.Support.subsupport_preStrong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : S.Subsupport S.preStrong

theorem ConNF.Support.preStrong_atoms [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) : (S.preStrong ⇘. A)ᴬ = (S ⇘. A)ᴬ + ((S + S.constrainsNearLitters).constrainsAtoms ⇘. A)ᴬ

theorem ConNF.Support.preStrong_nearLitters [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) (A : β ↝ ⊥) : (S.preStrong ⇘. A)ᴺ = (S ⇘. A)ᴺ + (S.constrainsNearLitters ⇘. A)ᴺ

theorem ConNF.Support.preStrong_preStrong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : S.preStrong.PreStrong

theorem ConNF.Support.interference_small [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : ConNF.Small {a : β ↝ ⊥ × ConNF.Atom | ∃ (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter), N₁ ∈ (S ⇘. a.1)ᴺ ∧ N₂ ∈ (S ⇘. a.1)ᴺ ∧ a.2 ∈ ConNF.interference N₁ N₂}

def ConNF.Support.interferenceSupport [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : ConNF.Support β

Equations

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

theorem ConNF.Support.mem_interferenceSupport_atoms [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ ⊥) (a : ConNF.Atom) : a ∈ (S.interferenceSupport ⇘. A)ᴬ ↔ ∃ N₁ ∈ (S ⇘. A)ᴺ, ∃ N₂ ∈ (S ⇘. A)ᴺ, a ∈ ConNF.interference N₁ N₂

theorem ConNF.Support.interferenceSupport_nearLitters [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ ⊥) : (S.interferenceSupport ⇘. A)ᴺ = ConNF.Enumeration.empty

def ConNF.Support.close [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : ConNF.Support β

Equations

• S.close = S + S.interferenceSupport

theorem ConNF.Support.subsupport_close [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : S.Subsupport S.close

theorem ConNF.Support.close_atoms [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ ⊥) : (S.close ⇘. A)ᴬ = (S ⇘. A)ᴬ + (S.interferenceSupport ⇘. A)ᴬ

theorem ConNF.Support.close_nearLitters [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) (A : β ↝ ⊥) : (S.close ⇘. A)ᴺ = (S ⇘. A)ᴺ

theorem ConNF.Support.close_closed [ConNF.Params] {β : ConNF.TypeIndex} (S : ConNF.Support β) : S.close.Closed

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

Equations

• S.strong = S.preStrong.close

theorem ConNF.Support.preStrong_subsupport_strong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : S.preStrong.Subsupport S.strong

theorem ConNF.Support.subsupport_strong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : S.Subsupport S.strong

theorem ConNF.Support.strong_strong [ConNF.Params] {β : ConNF.TypeIndex} [ConNF.Level] [ConNF.CoherentData] [ConNF.LeLevel β] (S : ConNF.Support β) : S.strong.Strong