Equations
- ConNF.Support.instFOAAssumptions = ConNF.MainInduction.FOA.foaAssumptions
Instances For
theorem
ConNF.Support.toPath_comp_eq_cons
[ConNF.Params]
{α : ConNF.TypeIndex}
{β : ConNF.TypeIndex}
{γ : ConNF.TypeIndex}
{δ : ConNF.TypeIndex}
(hβ : β < α)
(hγ : γ < α)
(hδ : δ < γ)
(A : Quiver.Path β δ)
(B : Quiver.Path α γ)
(h : (Quiver.Hom.toPath hβ).comp A = B.cons hδ)
:
∃ (C : Quiver.Path β γ), B = (Quiver.Hom.toPath hβ).comp C
theorem
ConNF.Support.raise_eq_cons_cons
[ConNF.Params]
{α : ConNF.Λ}
{β : ConNF.Λ}
{γ : ConNF.Λ}
{δ : ConNF.Λ}
(hβ : ↑β < ↑α)
(hδ : ↑δ < ↑γ)
(c : ConNF.Address ↑β)
(B : Quiver.Path ↑α ↑γ)
(x : ConNF.Atom ⊕ ConNF.NearLitter)
(h : ConNF.raise hβ c = { path := (B.cons hδ).cons ⋯, value := x })
:
γ = α ∨ ∃ (C : Quiver.Path ↑β ↑γ), B = (Quiver.Hom.toPath hβ).comp C
theorem
ConNF.Support.eq_raiseIndex_of_zero_lt_length
[ConNF.Params]
{β : ConNF.Λ}
{δ : ConNF.TypeIndex}
{A : Quiver.Path (↑β) δ}
(h : 0 < A.length)
:
∃ (γ : ConNF.TypeIndex) (hγ : γ < ↑β) (B : Quiver.Path γ δ), A = (Quiver.Hom.toPath hγ).comp B
theorem
ConNF.Support.eq_raiseIndex_of_one_lt_length
[ConNF.Params]
{β : ConNF.Λ}
{A : ConNF.ExtendedIndex ↑β}
(h : 1 < Quiver.Path.length A)
:
∃ (γ : ConNF.Λ) (hγ : ↑γ < ↑β) (B : ConNF.ExtendedIndex ↑γ), A = (Quiver.Hom.toPath hγ).comp B
theorem
ConNF.Support.eq_raise_of_one_lt_length
[ConNF.Params]
{β : ConNF.Λ}
{c : ConNF.Address ↑β}
(h : 1 < Quiver.Path.length c.path)
:
∃ (γ : ConNF.Λ) (hγ : ↑γ < ↑β) (d : ConNF.Address ↑γ), c = ConNF.raise hγ d
theorem
ConNF.Support.zero_lt_length
[ConNF.Params]
{γ : ConNF.Λ}
(A : ConNF.ExtendedIndex ↑γ)
:
0 < Quiver.Path.length A
theorem
ConNF.Support.precedes_raise
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
{c : ConNF.Address ↑β}
{d : ConNF.Address ↑γ}
(h : ConNF.Support.Precedes c (ConNF.raise hγ d))
:
1 < Quiver.Path.length c.path ∨ ∃ (a : ConNF.Atom), c = { path := Quiver.Hom.toPath ⋯, value := Sum.inl a }
@[simp]
theorem
ConNF.Support.raiseIndex_length
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(A : ConNF.ExtendedIndex ↑γ)
:
Quiver.Path.length (ConNF.raiseIndex hγ A) = Quiver.Path.length A + 1
theorem
ConNF.Support.precClosure_raise_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(T : ConNF.Support ↑γ)
(c : ConNF.Address ↑β)
(h : c ∈ ConNF.Support.precClosure (ConNF.Enumeration.image T (ConNF.raise hγ)).carrier)
:
1 < Quiver.Path.length c.path ∨ ∃ (a : ConNF.Atom), c = { path := Quiver.Hom.toPath ⋯, value := Sum.inl a }
theorem
ConNF.Support.strongSupport_raise_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
(hγ : ↑γ < ↑β)
(T : ConNF.Support ↑γ)
(c : ConNF.Address ↑β)
(h : c ∈ ConNF.Support.strongSupport ⋯)
:
1 < Quiver.Path.length c.path ∨ ∃ (a : ConNF.Atom), c = { path := Quiver.Hom.toPath ⋯, value := Sum.inl a }
theorem
ConNF.Support.path_eq_nil'
[ConNF.Params]
{α : ConNF.TypeIndex}
{β : ConNF.TypeIndex}
(h : α = β)
(p : Quiver.Path α β)
:
p.length = 0
theorem
ConNF.Support.raise_smul_raise_strong
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(T : ConNF.Support ↑γ)
(ρ : ConNF.Allowable ↑β)
:
def
ConNF.Support.interference
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
:
Set (ConNF.Address ↑β)
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
ConNF.Support.interference'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
:
Set (ConNF.Address ↑β)
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
ConNF.Support.interference_eq_interference'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
:
ConNF.Support.interference hγ S T = ConNF.Support.interference' hγ S T
theorem
ConNF.Support.interference_small
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
:
ConNF.Small (ConNF.Support.interference hγ S T)
def
ConNF.Support.interferenceSupport
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
:
Equations
- ConNF.Support.interferenceSupport hγ S T = ConNF.Enumeration.ofSet (ConNF.Support.interference hγ S T) ⋯
Instances For
theorem
ConNF.Support.mem_interferenceSupport_iff
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
(c : ConNF.Address ↑β)
:
c ∈ ConNF.Support.interferenceSupport hγ S T ↔ c ∈ ConNF.Support.interference hγ S T
theorem
ConNF.Support.interferenceSupport_ne_nearLitter
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{N : ConNF.NearLitter}
{i : ConNF.κ}
(hi : i < (ConNF.Support.interferenceSupport hγ S T).max)
:
((ConNF.Support.interferenceSupport hγ S T).f i hi).value ≠ Sum.inr N
theorem
ConNF.Support.interferenceSupport_eq_atom
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{i : ConNF.κ}
(hi : i < (ConNF.Support.interferenceSupport hγ S T).max)
:
∃ (A : ConNF.ExtendedIndex ↑β) (a : ConNF.Atom),
(ConNF.Support.interferenceSupport hγ S T).f i hi = { path := A, value := Sum.inl a }
def
ConNF.Support.raiseRaise
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
(hγ : ↑γ < ↑β)
(S : ConNF.Support ↑ConNF.α)
(T : ConNF.Support ↑γ)
(ρ : ConNF.Allowable ↑β)
:
ConNF.Support ↑ConNF.α
Equations
- ConNF.Support.raiseRaise hγ S T ρ = S + ConNF.Enumeration.image (ρ • (ConNF.Support.strongSupport ⋯ + ConNF.Support.interferenceSupport hγ S T)) (ConNF.raise ⋯)
Instances For
theorem
ConNF.Support.raiseRaise_max
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
:
(ConNF.Support.raiseRaise hγ S T ρ).max = S.max + ((ConNF.Support.strongSupport ⋯).max + (ConNF.Support.interferenceSupport hγ S T).max)
theorem
ConNF.Support.raiseRaise_hi₁
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < S.max)
:
i < (ConNF.Support.raiseRaise hγ S T ρ).max
theorem
ConNF.Support.raiseRaise_hi₂
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < S.max + (ConNF.Support.strongSupport ⋯).max)
:
i < (ConNF.Support.raiseRaise hγ S T ρ).max
theorem
ConNF.Support.raiseRaise_hi₂'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{i : ConNF.κ}
(hi₁ : S.max ≤ i)
(hi₂ : i < S.max + (ConNF.Support.strongSupport ⋯).max)
:
i - S.max < (ConNF.Support.strongSupport ⋯).max
theorem
ConNF.Support.raiseRaise_hi₃'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi₁ : S.max + (ConNF.Support.strongSupport ⋯).max ≤ i)
(hi₂ : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
:
i - S.max - (ConNF.Support.strongSupport ⋯).max < (ConNF.Support.interferenceSupport hγ S T).max
theorem
ConNF.Support.raiseRaise_f_eq₁
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < S.max)
:
(ConNF.Support.raiseRaise hγ S T ρ).f i ⋯ = S.f i hi
theorem
ConNF.Support.raiseRaise_f_eq₂
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi₁ : S.max ≤ i)
(hi₂ : i < S.max + (ConNF.Support.strongSupport ⋯).max)
:
(ConNF.Support.raiseRaise hγ S T ρ).f i ⋯ = ConNF.raise ⋯ (ρ • (ConNF.Support.strongSupport ⋯).f (i - S.max) ⋯)
theorem
ConNF.Support.raiseRaise_f_eq₃
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi₁ : S.max + (ConNF.Support.strongSupport ⋯).max ≤ i)
(hi₂ : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
:
(ConNF.Support.raiseRaise hγ S T ρ).f i hi₂ = ConNF.raise ⋯ (ρ • (ConNF.Support.interferenceSupport hγ S T).f (i - S.max - (ConNF.Support.strongSupport ⋯).max) ⋯)
theorem
ConNF.Support.raiseRaise_cases
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
:
i < S.max ∨ S.max ≤ i ∧ i < S.max + (ConNF.Support.strongSupport ⋯).max ∨ S.max + (ConNF.Support.strongSupport ⋯).max ≤ i ∧ i < (ConNF.Support.raiseRaise hγ S T ρ).max
theorem
ConNF.Support.raiseIndex_of_raise_eq
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{c : ConNF.Address ↑β}
{d : ConNF.Address ↑ConNF.α}
(h : ConNF.raise ⋯ c = d)
:
∃ (A : ConNF.ExtendedIndex ↑β), ConNF.raiseIndex ⋯ A = d.path
theorem
ConNF.Support.raise_injective'
[ConNF.Params]
{β : ConNF.Λ}
{γ : ConNF.Λ}
{hγ : ↑γ < ↑β}
{c : ConNF.Address ↑γ}
{A : ConNF.ExtendedIndex ↑γ}
{x : ConNF.Atom ⊕ ConNF.NearLitter}
(h : ConNF.raise hγ c = { path := ConNF.raiseIndex hγ A, value := x })
:
c = { path := A, value := x }
theorem
ConNF.Support.raiseRaise_strong
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
:
(ConNF.Support.raiseRaise hγ S T ρ).Strong
theorem
ConNF.Support.raiseRaise_max_eq_max
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
:
(ConNF.Support.raiseRaise hγ S T 1).max = (ConNF.Support.raiseRaise hγ S T ρ).max
theorem
ConNF.Support.raiseRaise_ne_nearLitter
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi₁ : S.max + (ConNF.Support.strongSupport ⋯).max ≤ i)
(hi₂ : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N : ConNF.NearLitter}
:
(ConNF.Support.raiseRaise hγ S T ρ).f i hi₂ ≠ { path := A, value := Sum.inr N }
theorem
ConNF.Support.raiseRaise_f_eq_atom
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(a : ConNF.Atom)
(ha : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inl a })
:
∃ (b : ConNF.Atom), (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inl b }
theorem
ConNF.Support.raiseRaise_f_eq_nearLitter
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(N : ConNF.NearLitter)
(hN : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inr N })
:
∃ (N' : ConNF.NearLitter), (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inr N' }
theorem
ConNF.Support.raiseRaise_cases_nearLitter
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(h₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inr N₁ })
(h₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inr N₂ })
:
i < S.max ∨ S.max ≤ i ∧ i < S.max + (ConNF.Support.strongSupport ⋯).max ∧ ∃ (B : ConNF.ExtendedIndex ↑β), A = ConNF.raiseIndex ⋯ B
theorem
ConNF.Support.raiseRaise_cases'
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
(ρ₁ : ConNF.Allowable ↑β)
(ρ₂ : ConNF.Allowable ↑β)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{x : ConNF.Atom ⊕ ConNF.NearLitter}
(h : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := x })
:
(ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := x } ∨ ∃ (B : ConNF.ExtendedIndex ↑β),
A = ConNF.raiseIndex ⋯ B ∧ (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := ConNF.Allowable.toStructPerm (ρ₂ * ρ₁⁻¹) B • x }
TODO: Use this lemma more! (All the lemmas tagged with this TODO should be put to use in the atom_spec case.)
theorem
ConNF.Support.raiseRaise_raiseIndex
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑β}
{x : ConNF.Atom ⊕ ConNF.NearLitter}
(h : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := ConNF.raiseIndex ⋯ A, value := x })
:
(ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := ConNF.raiseIndex ⋯ A, value := ConNF.Allowable.toStructPerm (ρ₂ * ρ₁⁻¹) A • x }
TODO: Use this lemma more!
theorem
ConNF.Support.raiseRaise_not_raiseIndex
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
(ρ₂ : ConNF.Allowable ↑β)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
(hA : ¬∃ (B : ConNF.ExtendedIndex ↑β), A = ConNF.raiseIndex ⋯ B)
{x : ConNF.Atom ⊕ ConNF.NearLitter}
(h : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := x })
:
(ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := x }
TODO: Use this lemma more!
theorem
ConNF.Support.raiseRaise_inflexibleCoe₃
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : S.max ≤ i)
(hi' : i < S.max + (ConNF.Support.strongSupport ⋯).max)
{A : ConNF.ExtendedIndex ↑β}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(h₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₁ })
(h₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₂ })
(h : ConNF.InflexibleCoe (ConNF.raiseIndex ⋯ A) N₁.fst)
:
∃ (P : ConNF.InflexibleCoePath A) (t : ConNF.Tangle ↑P.δ),
N₁.fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (P.B.cons ⋯)) ρ₁ • t) ∧ N₂.fst = ConNF.fuzz ⋯ ((ConNF.Allowable.comp (P.B.cons ⋯)) ρ₂ • t)
theorem
ConNF.Support.raiseRaise_inflexibleBot₃
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : S.max ≤ i)
(hi' : i < S.max + (ConNF.Support.strongSupport ⋯).max)
{A : ConNF.ExtendedIndex ↑β}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(h₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₁ })
(h₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₂ })
(h : ConNF.InflexibleBot (ConNF.raiseIndex ⋯ A) N₁.fst)
:
∃ (P : ConNF.InflexibleBotPath A) (a : ConNF.Atom),
N₁.fst = ConNF.fuzz ⋯ (ConNF.Allowable.toStructPerm ρ₁ (P.B.cons ⋯) • a) ∧ N₂.fst = ConNF.fuzz ⋯ (ConNF.Allowable.toStructPerm ρ₂ (P.B.cons ⋯) • a)
theorem
ConNF.Support.raiseRaise_flexible₃
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : S.max ≤ i)
(hi' : i < S.max + (ConNF.Support.strongSupport ⋯).max)
{A : ConNF.ExtendedIndex ↑β}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(h₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₁ })
(h₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i ⋯ = { path := ConNF.raiseIndex ⋯ A, value := Sum.inr N₂ })
(h : ConNF.Flexible (ConNF.raiseIndex ⋯ A) N₁.fst)
:
ConNF.Flexible (ConNF.raiseIndex ⋯ A) N₂.fst
theorem
ConNF.Support.raiseRaise_eq_cases
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max}
{c : ConNF.Address ↑ConNF.α}
(h : (ConNF.Support.raiseRaise hγ S T ρ).f i hi = c)
:
(∃ (d : ConNF.Address ↑β), c = ConNF.raise ⋯ (ρ • d) ∧ (ConNF.Support.raiseRaise hγ S T 1).f i hi = ConNF.raise ⋯ d) ∨ c ∈ S ∧ (ConNF.Support.raiseRaise hγ S T 1).f i hi = c
theorem
ConNF.Support.raiseRaise_atom_spec₁_raise
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρ₁S : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ (ρ₁ • c) ∈ S → ρ₁ • c = ρ₂ • c)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{a₁ : ConNF.Atom}
{a₂ : ConNF.Atom}
{c : ConNF.Address ↑β}
(ha₁ : ConNF.raise ⋯ (ρ₁ • c) = { path := A, value := Sum.inl a₁ })
(ha₂ : ConNF.raise ⋯ (ρ₂ • c) = { path := A, value := Sum.inl a₂ })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inl a₁ }} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inl a₂ }}
theorem
ConNF.Support.raiseRaise_atom_spec₁
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρ₁S : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ (ρ₁ • c) ∈ S → ρ₁ • c = ρ₂ • c)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{a₁ : ConNF.Atom}
{a₂ : ConNF.Atom}
(ha₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inl a₁ })
(ha₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inl a₂ })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inl a₁ }} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inl a₂ }}
theorem
ConNF.Support.raiseRaise_atom_spec₂_raise
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{a₁ : ConNF.Atom}
{a₂ : ConNF.Atom}
{c : ConNF.Address ↑β}
(ha₁ : ConNF.raise ⋯ (ρ₁ • c) = { path := A, value := Sum.inl a₁ })
(ha₂ : ConNF.raise ⋯ (ρ₂ • c) = { path := A, value := Sum.inl a₂ })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max) (N : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inr N } ∧ a₁ ∈ N} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max) (N : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inr N } ∧ a₂ ∈ N}
theorem
ConNF.Support.raiseRaise_atom_spec₂
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{a₁ : ConNF.Atom}
{a₂ : ConNF.Atom}
(ha₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inl a₁ })
(ha₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inl a₂ })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max) (N : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inr N } ∧ a₁ ∈ N} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max) (N : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inr N } ∧ a₂ ∈ N}
theorem
ConNF.Support.raiseRaise_flexibleCoe_spec_eq
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{i : ConNF.κ}
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(hN₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inr N₁ })
(hN₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inr N₂ })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max) (N' : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inr N' } ∧ N'.fst = N₁.fst} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max) (N' : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inr N' } ∧ N'.fst = N₂.fst}
theorem
ConNF.Support.raiseRaise_inflexibleCoe_spec₁_comp_before_aux
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < S.max)
{j : ConNF.κ}
(hji : j < i)
:
((ConNF.Support.raiseRaise hγ S T ρ₁).before i ⋯).f j hji = ((ConNF.Support.raiseRaise hγ S T ρ₂).before i ⋯).f j hji
theorem
ConNF.Support.raiseRaise_inflexibleCoe_spec₁_comp_before
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
{i : ConNF.κ}
(hi : i < S.max)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N : ConNF.NearLitter}
(h : ConNF.InflexibleCoe A N.fst)
:
∃ (ρ : ConNF.Allowable ↑h.path.δ),
((ConNF.Support.raiseRaise hγ S T ρ₁).before i ⋯).comp (h.path.B.cons ⋯) = ρ • ((ConNF.Support.raiseRaise hγ S T ρ₂).before i ⋯).comp (h.path.B.cons ⋯) ∧ h.t.set = ρ • h.t.set
theorem
ConNF.Support.raiseRaise_inflexibleCoe_spec₂_comp_before
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{i : ConNF.κ}
(hi' : i < S.max + (ConNF.Support.strongSupport ⋯).max)
{A : ConNF.ExtendedIndex ↑β}
(P : ConNF.InflexibleCoePath A)
(t : ConNF.Tangle ↑P.δ)
:
∃ (ρ' : ConNF.Allowable ↑P.δ),
((ConNF.Support.raiseRaise hγ S T ρ).before i ⋯).comp (((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯) = ρ' • ((ConNF.Support.raiseRaise hγ S T 1).before i ⋯).comp (((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯) ∧ (ConNF.Allowable.comp (P.B.cons ⋯)) ρ • t.set = ρ' • t.set
theorem
ConNF.Support.raiseRaise_symmDiff
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{i : ConNF.κ}
{hi : i < (ConNF.Support.raiseRaise hγ S T ρ₁).max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N₁ : ConNF.NearLitter}
{N₂ : ConNF.NearLitter}
(hN₁ : (ConNF.Support.raiseRaise hγ S T ρ₁).f i hi = { path := A, value := Sum.inr N₁ })
(hN₂ : (ConNF.Support.raiseRaise hγ S T ρ₂).f i hi = { path := A, value := Sum.inr N₂ })
(j : ConNF.κ)
:
{k : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₁).max) (a :
ConNF.Atom) (N' : ConNF.NearLitter),
N'.fst = N₁.fst ∧ a ∈ symmDiff ↑N₁ ↑N' ∧ (ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := A, value := Sum.inr N' } ∧ (ConNF.Support.raiseRaise hγ S T ρ₁).f k hk = { path := A, value := Sum.inl a }} ⊆ {k : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₂).max) (a :
ConNF.Atom) (N' : ConNF.NearLitter),
N'.fst = N₂.fst ∧ a ∈ symmDiff ↑N₂ ↑N' ∧ (ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := A, value := Sum.inr N' } ∧ (ConNF.Support.raiseRaise hγ S T ρ₂).f k hk = { path := A, value := Sum.inl a }}
theorem
ConNF.Support.raiseRaise_inflexibleCoe_spec₁_support
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N : ConNF.NearLitter}
(h : ConNF.InflexibleCoe A N.fst)
{i : ConNF.κ}
{hi : i < S.max}
(hN : S.f i hi = { path := A, value := Sum.inr N })
(j : ConNF.κ)
:
{k : ConNF.κ |
∃ (hj : j < h.t.support.max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
{ path := (h.path.B.cons ⋯).comp (h.t.support.f j hj).path, value := (h.t.support.f j hj).value } = (ConNF.Support.raiseRaise hγ S T ρ₁).f k hk} ⊆ {k : ConNF.κ |
∃ (hj : j < h.t.support.max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
{ path := (h.path.B.cons ⋯).comp (h.t.support.f j hj).path, value := (h.t.support.f j hj).value } = (ConNF.Support.raiseRaise hγ S T ρ₂).f k hk}
theorem
ConNF.Support.raiseRaise_inflexibleCoe_spec₂_support
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{A : ConNF.ExtendedIndex ↑β}
(P : ConNF.InflexibleCoePath A)
(t : ConNF.Tangle ↑P.δ)
(j : ConNF.κ)
:
{k : ConNF.κ |
∃ (hj : j < t.support.max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
{ path := (((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯).comp (t.support.f j hj).path,
value := (((ConNF.Allowable.comp (P.B.cons ⋯)) ρ₁ • t).support.f j hj).value } = (ConNF.Support.raiseRaise hγ S T ρ₁).f k hk} ⊆ {k : ConNF.κ |
∃ (hj : j < t.support.max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
{ path := (((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯).comp (t.support.f j hj).path,
value := (((ConNF.Allowable.comp (P.B.cons ⋯)) ρ₂ • t).support.f j hj).value } = (ConNF.Support.raiseRaise hγ S T ρ₂).f k hk}
theorem
ConNF.Support.raiseRaise_inflexibleBot_spec₁_atom
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{i : ConNF.κ}
{hi : i < S.max}
{A : ConNF.ExtendedIndex ↑ConNF.α}
{N : ConNF.NearLitter}
(h : ConNF.InflexibleBot A N.fst)
(hN : S.f i hi = { path := A, value := Sum.inr N })
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := h.path.B.cons ⋯, value := Sum.inl h.a }} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := h.path.B.cons ⋯, value := Sum.inl h.a }}
theorem
ConNF.Support.raiseRaise_inflexibleBot_spec₂_atom
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ₁ : ConNF.Allowable ↑β}
{ρ₂ : ConNF.Allowable ↑β}
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ₁⁻¹ • c = ρ₂⁻¹ • c)
{A : ConNF.ExtendedIndex ↑β}
(P : ConNF.InflexibleBotPath A)
(a : ConNF.Atom)
:
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₁).max),
(ConNF.Support.raiseRaise hγ S T ρ₁).f j hj = { path := ((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯,
value := Sum.inl (ConNF.Allowable.toStructPerm ρ₁ (P.B.cons ⋯) • a) }} ⊆ {j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ₂).max),
(ConNF.Support.raiseRaise hγ S T ρ₂).f j hj = { path := ((Quiver.Hom.toPath ⋯).comp P.B).cons ⋯,
value := Sum.inl (ConNF.Allowable.toStructPerm ρ₂ (P.B.cons ⋯) • a) }}
theorem
ConNF.Support.raiseRaise_specifies_atom_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{σ : ConNF.Spec ConNF.α}
(hσ : σ.Specifies (ConNF.Support.raiseRaise hγ S T 1) ⋯)
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(a : ConNF.Atom)
:
(ConNF.Support.raiseRaise hγ S T ρ).f i hi = { path := A, value := Sum.inl a } →
σ.f i ⋯ = ConNF.SpecCondition.atom A
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max),
(ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inl a }}
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max) (N : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inr N } ∧ a ∈ N}
theorem
ConNF.Support.raiseRaise_specifies_flexible_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{σ : ConNF.Spec ConNF.α}
(hσ : σ.Specifies (ConNF.Support.raiseRaise hγ S T 1) ⋯)
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(N₁ : ConNF.NearLitter)
:
ConNF.Flexible A N₁.fst →
(ConNF.Support.raiseRaise hγ S T ρ).f i hi = { path := A, value := Sum.inr N₁ } →
σ.f i ⋯ = ConNF.SpecCondition.flexible A
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max) (N' : ConNF.NearLitter),
(ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inr N' } ∧ N'.fst = N₁.fst}
fun (j : ConNF.κ) =>
{k : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ).max) (a :
ConNF.Atom) (N' : ConNF.NearLitter),
N'.fst = N₁.fst ∧ a ∈ symmDiff ↑N₁ ↑N' ∧ (ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inr N' } ∧ (ConNF.Support.raiseRaise hγ S T ρ).f k hk = { path := A, value := Sum.inl a }}
theorem
ConNF.Support.raiseRaise_specifies_inflexibleCoe_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{σ : ConNF.Spec ConNF.α}
(hσ : σ.Specifies (ConNF.Support.raiseRaise hγ S T 1) ⋯)
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(N₁ : ConNF.NearLitter)
(h : ConNF.InflexibleCoe A N₁.fst)
(hN₁ : (ConNF.Support.raiseRaise hγ S T ρ).f i hi = { path := A, value := Sum.inr N₁ })
:
σ.f i ⋯ = ConNF.SpecCondition.inflexibleCoe A h.path
(ConNF.CodingFunction.code (((ConNF.Support.raiseRaise hγ S T ρ).before i hi).comp (h.path.B.cons ⋯)) h.t.set ⋯)
(fun (j : ConNF.κ) =>
{k : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ).max) (a :
ConNF.Atom) (N' : ConNF.NearLitter),
N'.fst = N₁.fst ∧ a ∈ symmDiff ↑N₁ ↑N' ∧ (ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inr N' } ∧ (ConNF.Support.raiseRaise hγ S T ρ).f k hk = { path := A, value := Sum.inl a }})
h.t.support.max fun (j : ConNF.κ) =>
{k : ConNF.κ |
∃ (hj : j < h.t.support.max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ).max),
{ path := (h.path.B.cons ⋯).comp (h.t.support.f j hj).path, value := (h.t.support.f j hj).value } = (ConNF.Support.raiseRaise hγ S T ρ).f k hk}
theorem
ConNF.Support.raiseRaise_specifies_inflexibleBot_spec
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
{S : ConNF.Support ↑ConNF.α}
{T : ConNF.Support ↑γ}
{ρ : ConNF.Allowable ↑β}
(hS : S.Strong)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{σ : ConNF.Spec ConNF.α}
(hσ : σ.Specifies (ConNF.Support.raiseRaise hγ S T 1) ⋯)
(i : ConNF.κ)
(hi : i < (ConNF.Support.raiseRaise hγ S T ρ).max)
(A : ConNF.ExtendedIndex ↑ConNF.α)
(N₁ : ConNF.NearLitter)
(h : ConNF.InflexibleBot A N₁.fst)
:
(ConNF.Support.raiseRaise hγ S T ρ).f i hi = { path := A, value := Sum.inr N₁ } →
σ.f i ⋯ = ConNF.SpecCondition.inflexibleBot A h.path
{j : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max),
(ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := h.path.B.cons ⋯, value := Sum.inl h.a }}
fun (j : ConNF.κ) =>
{k : ConNF.κ |
∃ (hj : j < (ConNF.Support.raiseRaise hγ S T ρ).max) (hk : k < (ConNF.Support.raiseRaise hγ S T ρ).max) (a :
ConNF.Atom) (N' : ConNF.NearLitter),
N'.fst = N₁.fst ∧ a ∈ symmDiff ↑N₁ ↑N' ∧ (ConNF.Support.raiseRaise hγ S T ρ).f j hj = { path := A, value := Sum.inr N' } ∧ (ConNF.Support.raiseRaise hγ S T ρ).f k hk = { path := A, value := Sum.inl a }}
theorem
ConNF.Support.raiseRaise_specifies
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
{hγ : ↑γ < ↑β}
(S : ConNF.Support ↑ConNF.α)
(hS : S.Strong)
(T : ConNF.Support ↑γ)
(ρ : ConNF.Allowable ↑β)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
{σ : ConNF.Spec ConNF.α}
(hσ : σ.Specifies (ConNF.Support.raiseRaise hγ S T 1) ⋯)
:
σ.Specifies (ConNF.Support.raiseRaise hγ S T ρ) ⋯
theorem
ConNF.Support.raiseRaise_eq_smul
[ConNF.Params]
[ConNF.Level]
{β : ConNF.Λ}
{γ : ConNF.Λ}
[iβ : ConNF.LtLevel ↑β]
[iγ : ConNF.LtLevel ↑γ]
{hγ : ↑γ < ↑β}
(S : ConNF.Support ↑ConNF.α)
(hS : S.Strong)
(T : ConNF.Support ↑γ)
(ρ : ConNF.Allowable ↑β)
(hρS : ∀ (c : ConNF.Address ↑β), ConNF.raise ⋯ c ∈ S → ρ • c = c)
:
∃ (ρ' : ConNF.Allowable ↑ConNF.α),
ρ' • S = S ∧ (ConNF.Allowable.comp ((Quiver.Hom.toPath ⋯).cons hγ)) ρ' • T = (ConNF.Allowable.comp (Quiver.Hom.toPath hγ)) ρ • T