Supports with the same specification #
In this file, we show that two strong supports with the same specification are related by an allowable permutation.
Main declarations #
ConNF.exists_conv: Two strong supports with the same specification are related by an allowable permutation.
theorem
ConNF.Support.atom_mem_of_mem_of_spec_eq_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
{a₁ a₂ : ConNF.Atom}
{N₁ N₂ : ConNF.NearLitter}
{A : β ↝ ⊥}
(ha : ConNF.convAtoms S T A a₁ a₂)
(hN : ConNF.convNearLitters S T A N₁ N₂)
(haN : a₁ ∈ N₁ᴬ)
:
theorem
ConNF.Support.atom_mem_iff_mem_of_spec_eq_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
{a₁ a₂ : ConNF.Atom}
{N₁ N₂ : ConNF.NearLitter}
{A : β ↝ ⊥}
(ha : ConNF.convAtoms S T A a₁ a₂)
(hN : ConNF.convNearLitters S T A N₁ N₂)
:
theorem
ConNF.Support.litter_eq_litter_of_convNearLitters_of_spec_eq_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hT : T.Strong)
{N₁ N₂ N₃ N₄ : ConNF.NearLitter}
{A : β ↝ ⊥}
(hN₁₃ : ConNF.convNearLitters S T A N₁ N₃)
(hN₂₄ : ConNF.convNearLitters S T A N₂ N₄)
(hN₁₂ : N₁ᴸ = N₂ᴸ)
:
theorem
ConNF.Support.litter_eq_litter_iff_of_convNearLitters_of_spec_eq_spec
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
{N₁ N₂ N₃ N₄ : ConNF.NearLitter}
{A : β ↝ ⊥}
(hN₁₃ : ConNF.convNearLitters S T A N₁ N₃)
(hN₂₄ : ConNF.convNearLitters S T A N₂ N₄)
:
theorem
ConNF.Support.interference_subset_convAtoms_dom
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
{N₁ N₂ : ConNF.NearLitter}
{A : β ↝ ⊥}
(hN₁ : N₁ ∈ (ConNF.convNearLitters S T A).dom)
(hN₂ : N₂ ∈ (ConNF.convNearLitters S T A).dom)
:
ConNF.interference N₁ N₂ ⊆ (ConNF.convAtoms S T A).dom
theorem
ConNF.Support.interference_subset_convAtoms_codom
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hT : T.Strong)
{N₁ N₂ : ConNF.NearLitter}
{A : β ↝ ⊥}
(hN₁ : N₁ ∈ (ConNF.convNearLitters S T A).codom)
(hN₂ : N₂ ∈ (ConNF.convNearLitters S T A).codom)
:
ConNF.interference N₁ N₂ ⊆ (ConNF.convAtoms S T A).codom
def
ConNF.Support.convDeriv
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
(A : β ↝ ⊥)
:
ConNF.BaseAction
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[reducible, inline]
abbrev
ConNF.Support.conv
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
:
Equations
- ConNF.Support.conv hST hS hT = ConNF.Support.convDeriv hST hS hT
Instances For
theorem
ConNF.Support.conv_coherentAt
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
{A : β ↝ ⊥}
{N₁ N₂ : ConNF.NearLitter}
(hN : ConNF.convNearLitters S T A N₁ N₂)
:
ConNF.CoherentAt (ConNF.Support.conv hST hS hT) A N₁ᴸ N₂ᴸ
theorem
ConNF.Support.conv_coherent
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
:
(ConNF.Support.conv hST hS hT).Coherent
theorem
ConNF.Support.exists_conv
[ConNF.Params]
[ConNF.Level]
[ConNF.CoherentData]
{β : ConNF.TypeIndex}
[ConNF.LeLevel β]
{S T : ConNF.Support β}
(hST : S.spec = T.spec)
(hS : S.Strong)
(hT : T.Strong)
:
∃ (ρ : ConNF.AllPerm β), ρᵁ • S = T