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 [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} {A : β ↝ ⊥} (ha : convAtoms S T A a₁ a₂) (hN : convNearLitters S T A N₁ N₂) (haN : a₁ ∈ N₁ᴬ) : a₂ ∈ N₂ᴬ

theorem ConNF.Support.atom_mem_iff_mem_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} {A : β ↝ ⊥} (ha : convAtoms S T A a₁ a₂) (hN : convNearLitters S T A N₁ N₂) : a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ

theorem ConNF.Support.litter_eq_litter_of_convNearLitters_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hT : T.Strong) {N₁ N₂ N₃ N₄ : NearLitter} {A : β ↝ ⊥} (hN₁₃ : convNearLitters S T A N₁ N₃) (hN₂₄ : convNearLitters S T A N₂ N₄) (hN₁₂ : N₁ᴸ = N₂ᴸ) : N₃ᴸ = N₄ᴸ

theorem ConNF.Support.litter_eq_litter_iff_of_convNearLitters_of_spec_eq_spec [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) {N₁ N₂ N₃ N₄ : NearLitter} {A : β ↝ ⊥} (hN₁₃ : convNearLitters S T A N₁ N₃) (hN₂₄ : convNearLitters S T A N₂ N₄) : N₁ᴸ = N₂ᴸ ↔ N₃ᴸ = N₄ᴸ

theorem ConNF.Support.interference_subset_convAtoms_dom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) {N₁ N₂ : NearLitter} {A : β ↝ ⊥} (hN₁ : N₁ ∈ (convNearLitters S T A).dom) (hN₂ : N₂ ∈ (convNearLitters S T A).dom) : interference N₁ N₂ ⊆ (convAtoms S T A).dom

theorem ConNF.Support.interference_subset_convAtoms_codom [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hT : T.Strong) {N₁ N₂ : NearLitter} {A : β ↝ ⊥} (hN₁ : N₁ ∈ (convNearLitters S T A).codom) (hN₂ : N₂ ∈ (convNearLitters S T A).codom) : interference N₁ N₂ ⊆ (convAtoms S T A).codom

def ConNF.Support.convDeriv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) (A : β ↝ ⊥) : BaseAction

Equations

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

@[reducible, inline]

abbrev ConNF.Support.conv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) : StrAction β

Equations

• ConNF.Support.conv hST hS hT = ConNF.Support.convDeriv hST hS hT

theorem ConNF.Support.conv_coherentAt [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) {A : β ↝ ⊥} {N₁ N₂ : NearLitter} (hN : convNearLitters S T A N₁ N₂) : CoherentAt (conv hST hS hT) A N₁ᴸ N₂ᴸ

theorem ConNF.Support.conv_coherent [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) : (conv hST hS hT).Coherent

theorem ConNF.Support.exists_conv [Params] [Level] [CoherentData] {β : TypeIndex} [LeLevel β] {S T : Support β} (hST : S.spec = T.spec) (hS : S.Strong) (hT : T.Strong) : ∃ (ρ : AllPerm β), ρᵁ • S = T