Base actions

In this file, we define base actions.

Main declarations

• ConNF.BaseAction: The type of base actions.

structure ConNF.BaseAction [Params] : Type u

• atoms : Rel Atom Atom
• nearLitters : Rel NearLitter NearLitter
• atoms_dom_small' : Small self.atoms.dom
• nearLitters_dom_small' : Small self.nearLitters.dom
• atoms_oneOne' : self.atoms.OneOne
• mem_iff_mem' {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} : self.atoms a₁ a₂ → self.nearLitters N₁ N₂ → (a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ)
• litter_eq_litter_iff' {N₁ N₂ N₃ N₄ : NearLitter} : self.nearLitters N₁ N₃ → self.nearLitters N₂ N₄ → (N₁ᴸ = N₂ᴸ ↔ N₃ᴸ = N₄ᴸ)
• interference_subset_dom' {N₁ N₂ : NearLitter} : N₁ ∈ self.nearLitters.dom → N₂ ∈ self.nearLitters.dom → interference N₁ N₂ ⊆ self.atoms.dom
• interference_subset_codom' {N₁ N₂ : NearLitter} : N₁ ∈ self.nearLitters.codom → N₂ ∈ self.nearLitters.codom → interference N₁ N₂ ⊆ self.atoms.codom

theorem ConNF.BaseAction.mem_symmDiff_iff_mem_symmDiff [Params] {ξ : BaseAction} {a₁ a₂ : Atom} {N₁ N₂ N₃ N₄ : NearLitter} : ξ.atoms a₁ a₂ → ξ.nearLitters N₁ N₂ → ξ.nearLitters N₃ N₄ → (a₁ ∈ symmDiff N₁ᴬ N₃ᴬ ↔ a₂ ∈ symmDiff N₂ᴬ N₄ᴬ)

theorem ConNF.BaseAction.nearLitters_coinjective [Params] (ξ : BaseAction) : ξ.nearLitters.Coinjective

theorem ConNF.BaseAction.nearLitters_injective [Params] (ξ : BaseAction) : ξ.nearLitters.Injective

instance ConNF.BaseAction.instBaseActionClass [Params] : BaseActionClass BaseAction

Equations

• ConNF.BaseAction.instBaseActionClass = { atoms := ConNF.BaseAction.atoms, atoms_oneOne := ⋯, nearLitters := ConNF.BaseAction.nearLitters, nearLitters_oneOne := ⋯ }

theorem ConNF.BaseAction.ext [Params] {ξ ζ : BaseAction} (atoms : ξᴬ = ζᴬ) (nearLitters : ξᴺ = ζᴺ) : ξ = ζ

theorem ConNF.BaseAction.ext_iff [Params] {ξ ζ : BaseAction} : ξ = ζ ↔ ξᴬ = ζᴬ ∧ ξᴺ = ζᴺ

theorem ConNF.BaseAction.atoms_dom_small [Params] (ξ : BaseAction) : Small ξᴬ.dom

theorem ConNF.BaseAction.nearLitters_dom_small [Params] (ξ : BaseAction) : Small ξᴺ.dom

theorem ConNF.BaseAction.atoms_oneOne [Params] (ξ : BaseAction) : ξᴬ.OneOne

theorem ConNF.BaseAction.mem_iff_mem [Params] {ξ : BaseAction} {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} : ξᴬ a₁ a₂ → ξᴺ N₁ N₂ → (a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ)

theorem ConNF.BaseAction.litter_eq_litter_iff [Params] {ξ : BaseAction} {N₁ N₂ N₃ N₄ : NearLitter} : ξᴺ N₁ N₃ → ξᴺ N₂ N₄ → (N₁ᴸ = N₂ᴸ ↔ N₃ᴸ = N₄ᴸ)

theorem ConNF.BaseAction.interference_subset_dom [Params] {ξ : BaseAction} {N₁ N₂ : NearLitter} : N₁ ∈ ξᴺ.dom → N₂ ∈ ξᴺ.dom → interference N₁ N₂ ⊆ ξᴬ.dom

theorem ConNF.BaseAction.interference_subset_codom [Params] {ξ : BaseAction} {N₁ N₂ : NearLitter} : N₁ ∈ ξᴺ.codom → N₂ ∈ ξᴺ.codom → interference N₁ N₂ ⊆ ξᴬ.codom

theorem ConNF.BaseAction.atoms_codom_small [Params] (ξ : BaseAction) : Small ξᴬ.codom

theorem ConNF.BaseAction.nearLitters_codom_small [Params] (ξ : BaseAction) : Small ξᴺ.codom

def ConNF.BaseAction.inv [Params] (ξ : BaseAction) : BaseAction

Equations

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

instance ConNF.BaseAction.instInv [Params] : Inv BaseAction

Equations

• ConNF.BaseAction.instInv = { inv := ConNF.BaseAction.inv }

@[simp]

theorem ConNF.BaseAction.inv_atoms [Params] (ξ : BaseAction) : ξ⁻¹ᴬ = ξᴬ.inv

@[simp]

theorem ConNF.BaseAction.inv_nearLitters [Params] (ξ : BaseAction) : ξ⁻¹ᴺ = ξᴺ.inv

@[simp]

theorem ConNF.BaseAction.inv_inv [Params] (ξ : BaseAction) : ξ⁻¹⁻¹ = ξ

theorem ConNF.BaseAction.nearLitters_oneOne [Params] (ξ : BaseAction) : ξᴺ.OneOne

inductive ConNF.BaseAction.litters [Params] (ξ : BaseAction) : Rel Litter Litter

• mk [Params] {ξ : BaseAction} {N₁ N₂ : NearLitter} : ξᴺ N₁ N₂ → ξ.litters N₁ᴸ N₂ᴸ

instance ConNF.BaseAction.instSuperLRelLitter [Params] : SuperL BaseAction (Rel Litter Litter)

Equations

• ConNF.BaseAction.instSuperLRelLitter = { superL := ConNF.BaseAction.litters }

theorem ConNF.BaseAction.litters_iff [Params] {ξ : BaseAction} (L₁ L₂ : Litter) : ξᴸ L₁ L₂ ↔ ∃ (N₁ : NearLitter) (N₂ : NearLitter), N₁ᴸ = L₁ ∧ N₂ᴸ = L₂ ∧ ξᴺ N₁ N₂

theorem ConNF.BaseAction.litters_coinjective [Params] (ξ : BaseAction) : ξᴸ.Coinjective

theorem ConNF.BaseAction.litters_dom_small [Params] (ξ : BaseAction) : Small ξᴸ.dom

theorem ConNF.BaseAction.litters_codom_small [Params] (ξ : BaseAction) : Small ξᴸ.codom

@[simp]

theorem ConNF.BaseAction.inv_litters [Params] (ξ : BaseAction) : ξ⁻¹ᴸ = ξᴸ.inv

theorem ConNF.BaseAction.litters_injective [Params] (ξ : BaseAction) : ξᴸ.Injective

theorem ConNF.BaseAction.litters_oneOne [Params] (ξ : BaseAction) : ξᴸ.OneOne

instance ConNF.BaseAction.instLE [Params] : LE BaseAction

Equations

• ConNF.BaseAction.instLE = { le := fun (ξ ζ : ConNF.BaseAction) => ξᴬ ≤ ζᴬ ∧ ξᴺ = ζᴺ }

instance ConNF.BaseAction.instPartialOrder [Params] : PartialOrder BaseAction

Equations

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

theorem ConNF.BaseAction.litters_eq_of_le [Params] {ξ ζ : BaseAction} (h : ξ ≤ ζ) : ξᴸ = ζᴸ

theorem ConNF.BaseAction.inv_le_inv [Params] {ξ ζ : BaseAction} (h : ξ⁻¹ ≤ ζ⁻¹) : ξ ≤ ζ

theorem ConNF.BaseAction.inv_le [Params] {ξ ζ : BaseAction} (h : ξ⁻¹ ≤ ζ) : ξ ≤ ζ⁻¹

theorem ConNF.BaseAction.inv_le_inv_iff [Params] {ξ ζ : BaseAction} : ξ⁻¹ ≤ ζ⁻¹ ↔ ξ ≤ ζ

def ConNF.BaseAction.extend [Params] (ξ : BaseAction) (r : Rel Atom Atom) (r_dom_small : Small r.dom) (r_oneOne : r.OneOne) (r_dom_disjoint : Disjoint ξᴬ.dom r.dom) (r_codom_disjoint : Disjoint ξᴬ.codom r.codom) (r_mem_iff_mem : ∀ {a₁ a₂ : Atom} {N₁ N₂ : NearLitter}, r a₁ a₂ → ξᴺ N₁ N₂ → (a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ)) : BaseAction

A definition that can be used to reduce the proof obligations of extending a base action.

Equations

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

theorem ConNF.BaseAction.le_extend [Params] {ξ : BaseAction} {r : Rel Atom Atom} {r_dom_small : Small r.dom} {r_oneOne : r.OneOne} {r_dom_disjoint : Disjoint ξᴬ.dom r.dom} {r_codom_disjoint : Disjoint ξᴬ.codom r.codom} {r_mem_iff_mem : ∀ {a₁ a₂ : Atom} {N₁ N₂ : NearLitter}, r a₁ a₂ → ξᴺ N₁ N₂ → (a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ)} : ξ ≤ ξ.extend r r_dom_small r_oneOne r_dom_disjoint r_codom_disjoint ⋯

structure ConNF.BaseAction.Nice [Params] (ξ : BaseAction) : Prop

• symmDiff_subset_dom (N : NearLitter) : N ∈ ξᴺ.dom → symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.dom
• symmDiff_subset_codom (N : NearLitter) : N ∈ ξᴺ.codom → symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.codom

theorem ConNF.BaseAction.nice_iff [Params] (ξ : BaseAction) : ξ.Nice ↔ (∀ N ∈ ξᴺ.dom, symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.dom) ∧ ∀ N ∈ ξᴺ.codom, symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.codom

theorem ConNF.BaseAction.Nice.mem_litter_dom_iff [Params] {ξ : BaseAction} (h : ξ.Nice) {N : NearLitter} (hN : N ∈ ξᴺ.dom) {a : Atom} (ha : a ∉ ξᴬ.dom) : a ∈ Nᴬ ↔ aᴸ = Nᴸ

theorem ConNF.BaseAction.Nice.mem_litter_codom_iff [Params] {ξ : BaseAction} (h : ξ.Nice) {N : NearLitter} (hN : N ∈ ξᴺ.codom) {a : Atom} (ha : a ∉ ξᴬ.codom) : a ∈ Nᴬ ↔ aᴸ = Nᴸ

Extending orbits inside near-litters

def ConNF.BaseAction.inside [Params] (ξ : BaseAction) : Set Atom

The set of atoms contained in near-litters but not the corresponding litters.

Equations

• ξ.inside = {a : ConNF.Atom | ∃ N ∈ ξᴺ.dom, a ∈ Nᴬ ∧ aᴸ ≠ Nᴸ}

theorem ConNF.BaseAction.inside_small [Params] (ξ : BaseAction) : Small ξ.inside

structure ConNF.BaseAction.InsideCandidate [Params] (ξ : BaseAction) (L : Litter) (a : Atom) : Prop

• litter_eq : aᴸ = L
• not_mem_codom : a ∉ ξᴬ.codom
• mem_nearLitter {N : NearLitter} : N ∈ ξᴺ.codom → Nᴸ = L → a ∈ Nᴬ

theorem ConNF.BaseAction.insideCandidate_iff [Params] (ξ : BaseAction) (L : Litter) (a : Atom) : ξ.InsideCandidate L a ↔ aᴸ = L ∧ a ∉ ξᴬ.codom ∧ ∀ {N : NearLitter}, N ∈ ξᴺ.codom → Nᴸ = L → a ∈ Nᴬ

theorem ConNF.BaseAction.insideCandidates_not_small [Params] (ξ : BaseAction) (L : Litter) : ¬Small {a : Atom | ξ.InsideCandidate L a}

theorem ConNF.BaseAction.card_inside_lt_card_insideCandidates [Params] (ξ : BaseAction) (L : Litter) : Cardinal.mk ↑ξ.inside < Cardinal.mk ↑{a : Atom | ξ.InsideCandidate L a}

def ConNF.BaseAction.insideMap [Params] (ξ : BaseAction) (L : Litter) : ↑ξ.inside ↪ ↑{a : Atom | ξ.InsideCandidate L a}

Equations

• ξ.insideMap L = Nonempty.some ⋯

theorem ConNF.BaseAction.insideMap_litter_eq [Params] {ξ : BaseAction} (L : Litter) (x : ↑ξ.inside) : (↑((ξ.insideMap L) x))ᴸ = L

theorem ConNF.BaseAction.insideMap_not_mem_codom [Params] {ξ : BaseAction} (L : Litter) (x : ↑ξ.inside) : ↑((ξ.insideMap L) x) ∉ ξᴬ.codom

theorem ConNF.BaseAction.insideMap_mem_nearLitter [Params] {ξ : BaseAction} (L : Litter) (x : ↑ξ.inside) {N : NearLitter} : N ∈ ξᴺ.codom → Nᴸ = L → ↑((ξ.insideMap L) x) ∈ Nᴬ

def ConNF.BaseAction.insideRel [Params] (ξ : BaseAction) : Rel Atom Atom

Equations

• ξ.insideRel a₁ a₂ = ∃ (N₁ : ConNF.NearLitter) (N₂ : ConNF.NearLitter) (h : N₁ ∈ ξᴺ.dom ∧ a₁ ∈ N₁ᴬ ∧ a₁ᴸ ≠ N₁ᴸ), ξᴺ N₁ N₂ ∧ a₁ ∉ ξᴬ.dom ∧ a₂ = ↑((ξ.insideMap N₂ᴸ) ⟨a₁, ⋯⟩)

theorem ConNF.BaseAction.insideRel_dom_small [Params] (ξ : BaseAction) : Small ξ.insideRel.dom

theorem ConNF.BaseAction.insideRel_injective [Params] (ξ : BaseAction) : ξ.insideRel.Injective

theorem ConNF.BaseAction.insideRel_coinjective [Params] (ξ : BaseAction) : ξ.insideRel.Coinjective

theorem ConNF.BaseAction.insideRel_oneOne [Params] (ξ : BaseAction) : ξ.insideRel.OneOne

theorem ConNF.BaseAction.insideRel_dom [Params] (ξ : BaseAction) : Disjoint ξᴬ.dom ξ.insideRel.dom

theorem ConNF.BaseAction.insideRel_codom [Params] (ξ : BaseAction) : Disjoint ξᴬ.codom ξ.insideRel.codom

theorem ConNF.BaseAction.insideRel_mem_iff_mem [Params] {ξ : BaseAction} {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} (ha : ξ.insideRel a₁ a₂) (hN : ξᴺ N₁ N₂) : a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ

def ConNF.BaseAction.insideExtension [Params] (ξ : BaseAction) : BaseAction

Equations

• ξ.insideExtension = ξ.extend ξ.insideRel ⋯ ⋯ ⋯ ⋯ ⋯

theorem ConNF.BaseAction.insideExtension_atoms [Params] (ξ : BaseAction) : ξ.insideExtensionᴬ = ξᴬ ⊔ ξ.insideRel

theorem ConNF.BaseAction.le_insideExtension [Params] (ξ : BaseAction) : ξ ≤ ξ.insideExtension

theorem ConNF.BaseAction.insideExtension_spec [Params] {ξ : BaseAction} (N : NearLitter) (hN : N ∈ ξᴺ.dom) : Nᴬ \ Nᴸᴬ ⊆ ξ.insideExtensionᴬ.dom

Extending orbits outside near-litters

structure ConNF.BaseAction.Sandbox [Params] (ξ : BaseAction) (L : Litter) : Prop

• atom_not_mem (a : Atom) : a ∈ ξᴬ.codom → aᴸ ≠ L
• nearLitter_not_mem (N : NearLitter) (a : Atom) : aᴸ = L → N ∈ ξᴺ.codom → a ∉ Nᴬ

theorem ConNF.BaseAction.sandbox_iff [Params] (ξ : BaseAction) (L : Litter) : ξ.Sandbox L ↔ (∀ a ∈ ξᴬ.codom, aᴸ ≠ L) ∧ ∀ (N : NearLitter) (a : Atom), aᴸ = L → N ∈ ξᴺ.codom → a ∉ Nᴬ

def ConNF.BaseAction.not_sandbox_eq [Params] (ξ : BaseAction) : {L : Litter | ¬ξ.Sandbox L} = (⋃ a ∈ ξᴬ.codom, {aᴸ}) ∪ ⋃ N ∈ ξᴺ.codom, ⋃ a ∈ Nᴬ, {aᴸ}

Equations

• ⋯ = ⋯

theorem ConNF.BaseAction.card_not_sandbox [Params] (ξ : BaseAction) : Cardinal.mk ↑{L : Litter | ¬ξ.Sandbox L} ≤ Cardinal.mk κ

theorem ConNF.BaseAction.exists_sandbox [Params] (ξ : BaseAction) : {L : Litter | ξ.Sandbox L}.Nonempty

def ConNF.BaseAction.sandbox [Params] (ξ : BaseAction) : Litter

Equations

• ξ.sandbox = ⋯.some

theorem ConNF.BaseAction.sandbox_spec [Params] (ξ : BaseAction) : ξ.Sandbox ξ.sandbox

def ConNF.BaseAction.outside [Params] (ξ : BaseAction) : Set Atom

Equations

• ξ.outside = {a : ConNF.Atom | ∃ N ∈ ξᴺ.dom, a ∉ Nᴬ ∧ aᴸ = Nᴸ}

theorem ConNF.BaseAction.outside_small [Params] (ξ : BaseAction) : Small ξ.outside

theorem ConNF.BaseAction.card_outside_lt_card_sandbox [Params] (ξ : BaseAction) : Cardinal.mk ↑ξ.outside < Cardinal.mk ↑ξ.sandboxᴬ

def ConNF.BaseAction.outsideMap [Params] (ξ : BaseAction) : ↑ξ.outside ↪ ↑ξ.sandboxᴬ

Equations

• ξ.outsideMap = Nonempty.some ⋯

theorem ConNF.BaseAction.outsideMap_litter [Params] {ξ : BaseAction} (x : ↑ξ.outside) : ξ.Sandbox (↑(ξ.outsideMap x))ᴸ

def ConNF.BaseAction.outsideRel [Params] (ξ : BaseAction) : Rel Atom Atom

Equations

• ξ.outsideRel a₁ a₂ = (a₁ ∉ ξᴬ.dom ∧ ∃ (h : a₁ ∈ ξ.outside), a₂ = ↑(ξ.outsideMap ⟨a₁, h⟩))

theorem ConNF.BaseAction.outsideRel_dom_small [Params] (ξ : BaseAction) : Small ξ.outsideRel.dom

theorem ConNF.BaseAction.outsideRel_injective [Params] (ξ : BaseAction) : ξ.outsideRel.Injective

theorem ConNF.BaseAction.outsideRel_coinjective [Params] (ξ : BaseAction) : ξ.outsideRel.Coinjective

theorem ConNF.BaseAction.outsideRel_oneOne [Params] (ξ : BaseAction) : ξ.outsideRel.OneOne

theorem ConNF.BaseAction.outsideRel_dom [Params] (ξ : BaseAction) : Disjoint ξᴬ.dom ξ.outsideRel.dom

theorem ConNF.BaseAction.outsideRel_codom [Params] (ξ : BaseAction) : Disjoint ξᴬ.codom ξ.outsideRel.codom

theorem ConNF.BaseAction.outsideRel_mem_iff_mem [Params] {ξ : BaseAction} (hξ : ∀ N ∈ ξᴺ.dom, Nᴬ \ Nᴸᴬ ⊆ ξᴬ.dom) {a₁ a₂ : Atom} {N₁ N₂ : NearLitter} (ha : ξ.outsideRel a₁ a₂) (hN : ξᴺ N₁ N₂) : a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ

def ConNF.BaseAction.outsideExtension [Params] (ξ : BaseAction) (hξ : ∀ N ∈ ξᴺ.dom, Nᴬ \ Nᴸᴬ ⊆ ξᴬ.dom) : BaseAction

Equations

• ξ.outsideExtension hξ = ξ.extend ξ.outsideRel ⋯ ⋯ ⋯ ⋯ ⋯

theorem ConNF.BaseAction.outsideExtension_atoms [Params] (ξ : BaseAction) (hξ : ∀ N ∈ ξᴺ.dom, Nᴬ \ Nᴸᴬ ⊆ ξᴬ.dom) : (ξ.outsideExtension hξ)ᴬ = ξᴬ ⊔ ξ.outsideRel

theorem ConNF.BaseAction.le_outsideExtension [Params] (ξ : BaseAction) (hξ : ∀ N ∈ ξᴺ.dom, Nᴬ \ Nᴸᴬ ⊆ ξᴬ.dom) : ξ ≤ ξ.outsideExtension hξ

theorem ConNF.BaseAction.outsideExtension_spec [Params] {ξ : BaseAction} {hξ : ∀ N ∈ ξᴺ.dom, Nᴬ \ Nᴸᴬ ⊆ ξᴬ.dom} (N : NearLitter) (hN : N ∈ ξᴺ.dom) : Nᴸᴬ \ Nᴬ ⊆ (ξ.outsideExtension hξ)ᴬ.dom

Nice extensions

def ConNF.BaseAction.doubleInsideExtension [Params] (ξ : BaseAction) : BaseAction

Equations

• ξ.doubleInsideExtension = ξ.insideExtension⁻¹.insideExtension⁻¹

theorem ConNF.BaseAction.le_doubleInsideExtension [Params] (ξ : BaseAction) : ξ ≤ ξ.doubleInsideExtension

theorem ConNF.BaseAction.doubleInsideExtension_dom [Params] {ξ : BaseAction} (N : NearLitter) (hN : N ∈ ξᴺ.dom) : Nᴬ \ Nᴸᴬ ⊆ ξ.doubleInsideExtensionᴬ.dom

theorem ConNF.BaseAction.doubleInsideExtension_codom [Params] {ξ : BaseAction} (N : NearLitter) (hN : N ∈ ξᴺ.codom) : Nᴬ \ Nᴸᴬ ⊆ ξ.doubleInsideExtensionᴬ.codom

theorem ConNF.BaseAction.niceExtension_aux [Params] {ξ : BaseAction} (N : NearLitter) (hN : N ∈ ξᴺ.codom) : Nᴬ \ Nᴸᴬ ⊆ (ξ.doubleInsideExtension.outsideExtension ⋯)⁻¹ᴬ.dom

def ConNF.BaseAction.niceExtension [Params] (ξ : BaseAction) : BaseAction

Equations

• ξ.niceExtension = ((ξ.doubleInsideExtension.outsideExtension ⋯)⁻¹.outsideExtension ⋯)⁻¹

theorem ConNF.BaseAction.le_niceExtension [Params] (ξ : BaseAction) : ξ ≤ ξ.niceExtension

theorem ConNF.BaseAction.niceExtension_nice [Params] (ξ : BaseAction) : ξ.niceExtension.Nice

@[simp]

theorem ConNF.BaseAction.niceExtension_nearLitters [Params] (ξ : BaseAction) : ξ.niceExtensionᴺ = ξᴺ

@[simp]

theorem ConNF.BaseAction.niceExtension_litters [Params] (ξ : BaseAction) : ξ.niceExtensionᴸ = ξᴸ