Base actions

In this file, we define base actions.

Main declarations

• ConNF.BaseAction: The type of base actions.

structure ConNF.BaseAction [ConNF.Params] : Type u

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

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

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

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

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

Equations

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

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

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

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

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

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

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

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

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

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

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

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

Equations

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

Equations

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

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

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

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

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

@[simp]

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

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

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

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

Equations

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

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

Equations

• ConNF.BaseAction.instPartialOrder = PartialOrder.mk ⋯

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

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

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

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

def ConNF.BaseAction.extend [ConNF.Params] (ξ : ConNF.BaseAction) (r : Rel ConNF.Atom ConNF.Atom) (r_dom_small : ConNF.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₂ : ConNF.Atom} {N₁ N₂ : ConNF.NearLitter}, r a₁ a₂ → ξᴺ N₁ N₂ → (a₁ ∈ N₁ᴬ ↔ a₂ ∈ N₂ᴬ)) : ConNF.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 [ConNF.Params] {ξ : ConNF.BaseAction} {r : Rel ConNF.Atom ConNF.Atom} {r_dom_small : ConNF.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₂ : ConNF.Atom} {N₁ N₂ : ConNF.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 [ConNF.Params] (ξ : ConNF.BaseAction) : Prop

• symmDiff_subset_dom : ∀ N ∈ ξᴺ.dom, symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.dom
• symmDiff_subset_codom : ∀ N ∈ ξᴺ.codom, symmDiff Nᴬ Nᴸᴬ ⊆ ξᴬ.codom

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

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

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

Extending orbits inside near-litters

def ConNF.BaseAction.inside [ConNF.Params] (ξ : ConNF.BaseAction) : Set ConNF.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 [ConNF.Params] (ξ : ConNF.BaseAction) : ConNF.Small ξ.inside

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

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

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

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

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

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

Equations

• ξ.insideMap L = Nonempty.some ⋯

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

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

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

def ConNF.BaseAction.insideRel [ConNF.Params] (ξ : ConNF.BaseAction) : Rel ConNF.Atom ConNF.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 [ConNF.Params] (ξ : ConNF.BaseAction) : ConNF.Small ξ.insideRel.dom

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

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

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

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

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

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

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

Equations

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

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

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

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

Extending orbits outside near-litters

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

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

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

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

Equations

• ⋯ = ⋯

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

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

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

Equations

• ξ.sandbox = ⋯.some

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

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

Equations

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

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

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

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

Equations

• ξ.outsideMap = Nonempty.some ⋯

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

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

Equations

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

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

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

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

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

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

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

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

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

Equations

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

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

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

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

Nice extensions

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

Equations

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

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

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

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

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

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

Equations

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

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

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

@[simp]

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

@[simp]

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