Base near-litter actions

In this file, we define a slight variant of litter actions, called near-litter actions. They allow definition of the precise image of arbitrary near-litters, not just litters. This means that the lawfulness conditions are more complicated, but in exchange they are more useful to applications of the freedom of action theorem.

Main declarations

• ConNF.BaseNLAction: The type of base near-litter actions.
• ConNF.BaseNLAction.Lawful: Injectivity requirements that allow a near-litter action to be converted into an approximation.
• ConNF.BaseNLAction.Approximates: A base near-litter action approximates a base permutation if they agree wherever they are defined.
• ConNF.BaseNLAction.withLitters: Augments a near-litter action to define it on all litters near any near-litter in its domain. This allows us to create a litter action from it.
• ConNF.BaseNLAction.withLitters_lawful: The withLitters extension preserves lawfulness.

theorem ConNF.BaseNLAction.ext : ∀ {inst : ConNF.Params} (x y : ConNF.BaseNLAction), x.atomMap = y.atomMap → x.nearLitterMap = y.nearLitterMap → x = y

theorem ConNF.BaseNLAction.ext_iff : ∀ {inst : ConNF.Params} (x y : ConNF.BaseNLAction), x = y ↔ x.atomMap = y.atomMap ∧ x.nearLitterMap = y.nearLitterMap

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

• atomMap : ConNF.Atom →. ConNF.Atom
• nearLitterMap : ConNF.NearLitter →. ConNF.NearLitter
• atomMap_dom_small : ConNF.Small self.atomMap.Dom
• nearLitterMap_dom_small : ConNF.Small self.nearLitterMap.Dom

theorem ConNF.BaseNLAction.atomMap_dom_small [ConNF.Params] (self : ConNF.BaseNLAction) : ConNF.Small self.atomMap.Dom

theorem ConNF.BaseNLAction.nearLitterMap_dom_small [ConNF.Params] (self : ConNF.BaseNLAction) : ConNF.Small self.nearLitterMap.Dom

structure ConNF.BaseNLAction.Lawful [ConNF.Params] (ξ : ConNF.BaseNLAction) : Prop

• atomMap_injective : ∀ ⦃a b : ConNF.Atom⦄ (ha : (ξ.atomMap a).Dom) (hb : (ξ.atomMap b).Dom), (ξ.atomMap a).get ha = (ξ.atomMap b).get hb → a = b
• atom_mem_iff : ∀ ⦃a : ConNF.Atom⦄ (ha : (ξ.atomMap a).Dom) ⦃N : ConNF.NearLitter⦄ (hN : (ξ.nearLitterMap N).Dom), (ξ.atomMap a).get ha ∈ (ξ.nearLitterMap N).get hN ↔ a ∈ N
• dom_of_mem_symmDiff : ∀ (a : ConNF.Atom) ⦃N₁ N₂ : ConNF.NearLitter⦄, N₁.fst = N₂.fst → (ξ.nearLitterMap N₁).Dom → (ξ.nearLitterMap N₂).Dom → a ∈ symmDiff ↑N₁ ↑N₂ → (ξ.atomMap a).Dom
• dom_of_mem_inter : ∀ (a : ConNF.Atom) ⦃N₁ N₂ : ConNF.NearLitter⦄, N₁.fst ≠ N₂.fst → (ξ.nearLitterMap N₁).Dom → (ξ.nearLitterMap N₂).Dom → a ∈ ↑N₁ ∩ ↑N₂ → (ξ.atomMap a).Dom
• ran_of_mem_symmDiff : ∀ (a : ConNF.Atom) ⦃N₁ N₂ : ConNF.NearLitter⦄, N₁.fst = N₂.fst → ∀ (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), a ∈ symmDiff ↑((ξ.nearLitterMap N₁).get hN₁) ↑((ξ.nearLitterMap N₂).get hN₂) → a ∈ ξ.atomMap.ran
• ran_of_mem_inter : ∀ (a : ConNF.Atom) ⦃N₁ N₂ : ConNF.NearLitter⦄, N₁.fst ≠ N₂.fst → ∀ (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), a ∈ ↑((ξ.nearLitterMap N₁).get hN₁) ∩ ↑((ξ.nearLitterMap N₂).get hN₂) → a ∈ ξ.atomMap.ran

theorem ConNF.BaseNLAction.Lawful.atomMap_injective [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (ξ.atomMap a).Dom) (hb : (ξ.atomMap b).Dom) : (ξ.atomMap a).get ha = (ξ.atomMap b).get hb → a = b

theorem ConNF.BaseNLAction.Lawful.atom_mem_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) ⦃a : ConNF.Atom⦄ (ha : (ξ.atomMap a).Dom) ⦃N : ConNF.NearLitter⦄ (hN : (ξ.nearLitterMap N).Dom) : (ξ.atomMap a).get ha ∈ (ξ.nearLitterMap N).get hN ↔ a ∈ N

theorem ConNF.BaseNLAction.Lawful.dom_of_mem_symmDiff [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) (a : ConNF.Atom) ⦃N₁ : ConNF.NearLitter⦄ ⦃N₂ : ConNF.NearLitter⦄ : N₁.fst = N₂.fst → (ξ.nearLitterMap N₁).Dom → (ξ.nearLitterMap N₂).Dom → a ∈ symmDiff ↑N₁ ↑N₂ → (ξ.atomMap a).Dom

theorem ConNF.BaseNLAction.Lawful.dom_of_mem_inter [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) (a : ConNF.Atom) ⦃N₁ : ConNF.NearLitter⦄ ⦃N₂ : ConNF.NearLitter⦄ : N₁.fst ≠ N₂.fst → (ξ.nearLitterMap N₁).Dom → (ξ.nearLitterMap N₂).Dom → a ∈ ↑N₁ ∩ ↑N₂ → (ξ.atomMap a).Dom

theorem ConNF.BaseNLAction.Lawful.ran_of_mem_symmDiff [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) (a : ConNF.Atom) ⦃N₁ : ConNF.NearLitter⦄ ⦃N₂ : ConNF.NearLitter⦄ : N₁.fst = N₂.fst → ∀ (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), a ∈ symmDiff ↑((ξ.nearLitterMap N₁).get hN₁) ↑((ξ.nearLitterMap N₂).get hN₂) → a ∈ ξ.atomMap.ran

theorem ConNF.BaseNLAction.Lawful.ran_of_mem_inter [ConNF.Params] {ξ : ConNF.BaseNLAction} (self : ξ.Lawful) (a : ConNF.Atom) ⦃N₁ : ConNF.NearLitter⦄ ⦃N₂ : ConNF.NearLitter⦄ : N₁.fst ≠ N₂.fst → ∀ (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom), a ∈ ↑((ξ.nearLitterMap N₁).get hN₁) ∩ ↑((ξ.nearLitterMap N₂).get hN₂) → a ∈ ξ.atomMap.ran

theorem ConNF.BaseNLAction.approximates_iff [ConNF.Params] (ξ : ConNF.BaseNLAction) (π : ConNF.BasePerm) : ξ.Approximates π ↔ (∀ (a : ConNF.Atom) (h : (ξ.atomMap a).Dom), π • a = (ξ.atomMap a).get h) ∧ ∀ (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), π • N = (ξ.nearLitterMap N).get h

structure ConNF.BaseNLAction.Approximates [ConNF.Params] (ξ : ConNF.BaseNLAction) (π : ConNF.BasePerm) : Prop

• map_atom : ∀ (a : ConNF.Atom) (h : (ξ.atomMap a).Dom), π • a = (ξ.atomMap a).get h
• map_nearLitter : ∀ (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), π • N = (ξ.nearLitterMap N).get h

theorem ConNF.BaseNLAction.Approximates.map_atom [ConNF.Params] {ξ : ConNF.BaseNLAction} {π : ConNF.BasePerm} (self : ξ.Approximates π) (a : ConNF.Atom) (h : (ξ.atomMap a).Dom) : π • a = (ξ.atomMap a).get h

theorem ConNF.BaseNLAction.Approximates.map_nearLitter [ConNF.Params] {ξ : ConNF.BaseNLAction} {π : ConNF.BasePerm} (self : ξ.Approximates π) (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom) : π • N = (ξ.nearLitterMap N).get h

theorem ConNF.BaseNLAction.map_nearLitter_fst [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) ⦃N₁ : ConNF.NearLitter⦄ ⦃N₂ : ConNF.NearLitter⦄ (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) : N₁.fst = N₂.fst ↔ ((ξ.nearLitterMap N₁).get hN₁).fst = ((ξ.nearLitterMap N₂).get hN₂).fst

def ConNF.BaseNLAction.HasLitters [ConNF.Params] (ξ : ConNF.BaseNLAction) : Prop

Equations

• ξ.HasLitters = ∀ ⦃N : ConNF.NearLitter⦄, (ξ.nearLitterMap N).Dom → (ξ.nearLitterMap N.fst.toNearLitter).Dom

def ConNF.BaseNLAction.extraAtoms [ConNF.Params] (ξ : ConNF.BaseNLAction) : Set ConNF.Atom

Equations

• ξ.extraAtoms = ⋃ N ∈ ξ.nearLitterMap.Dom, ConNF.litterSet N.fst \ ↑N

theorem ConNF.BaseNLAction.extraAtoms_small [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Small ξ.extraAtoms

theorem ConNF.BaseNLAction.bannedLitter_iff [ConNF.Params] (ξ : ConNF.BaseNLAction) : ∀ (a : ConNF.Litter), ξ.BannedLitter a ↔ (∃ (a_1 : ConNF.Atom) (h : (ξ.atomMap a_1).Dom), a = ((ξ.atomMap a_1).get h).1) ∨ (∃ (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), a = ((ξ.nearLitterMap N).get h).fst) ∨ ∃ (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), ∃ a_1 ∈ ↑((ξ.nearLitterMap N).get h) \ ConNF.litterSet ((ξ.nearLitterMap N).get h).fst, a = a_1.1

inductive ConNF.BaseNLAction.BannedLitter [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Litter → Prop

• atomMap: ∀ [inst : ConNF.Params] {ξ : ConNF.BaseNLAction} (a : ConNF.Atom) (h : (ξ.atomMap a).Dom), ξ.BannedLitter ((ξ.atomMap a).get h).1
• nearLitterMap: ∀ [inst : ConNF.Params] {ξ : ConNF.BaseNLAction} (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), ξ.BannedLitter ((ξ.nearLitterMap N).get h).fst
• diff: ∀ [inst : ConNF.Params] {ξ : ConNF.BaseNLAction} (N : ConNF.NearLitter) (h : (ξ.nearLitterMap N).Dom), ∀ a ∈ ↑((ξ.nearLitterMap N).get h) \ ConNF.litterSet ((ξ.nearLitterMap N).get h).fst, ξ.BannedLitter a.1

theorem ConNF.BaseNLAction.bannedLitter_of_mem [ConNF.Params] {ξ : ConNF.BaseNLAction} (a : ConNF.Atom) (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) (ha : a ∈ (ξ.nearLitterMap N).get hN) : ξ.BannedLitter a.1

theorem ConNF.BaseNLAction.bannedLitter_small [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Small {L : ConNF.Litter | ξ.BannedLitter L}

theorem ConNF.BaseNLAction.mk_not_bannedLitter [ConNF.Params] (ξ : ConNF.BaseNLAction) : Cardinal.mk ↑{L : ConNF.Litter | ¬ξ.BannedLitter L} = Cardinal.mk ConNF.μ

theorem ConNF.BaseNLAction.not_bannedLitter_nonempty [ConNF.Params] (ξ : ConNF.BaseNLAction) : Nonempty ↑{L : ConNF.Litter | ¬ξ.BannedLitter L}

noncomputable def ConNF.BaseNLAction.sandboxLitter [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Litter

Equations

• ξ.sandboxLitter = ↑⋯.some

theorem ConNF.BaseNLAction.sandboxLitter_not_banned [ConNF.Params] (ξ : ConNF.BaseNLAction) : ¬ξ.BannedLitter ξ.sandboxLitter

def ConNF.BaseNLAction.LitterPresent [ConNF.Params] (ξ : ConNF.BaseNLAction) (L : ConNF.Litter) : Prop

Equations

• ξ.LitterPresent L = ∃ (N : ConNF.NearLitter), (ξ.nearLitterMap N).Dom ∧ N.fst = L

def ConNF.BaseNLAction.innerAtoms [ConNF.Params] (ξ : ConNF.BaseNLAction) (L : ConNF.Litter) : Set ConNF.Atom

Equations

• ξ.innerAtoms L = ⋂ (N : ConNF.NearLitter), ⋂ (_ : (ξ.nearLitterMap N).Dom ∧ N.fst = L), ↑N \ ConNF.litterSet L

def ConNF.BaseNLAction.outerAtoms [ConNF.Params] (ξ : ConNF.BaseNLAction) (L : ConNF.Litter) : Set ConNF.Atom

Equations

• ξ.outerAtoms L = ConNF.litterSet L \ ⋃ (N : ConNF.NearLitter), ⋃ (_ : (ξ.nearLitterMap N).Dom), ↑N

def ConNF.BaseNLAction.allOuterAtoms [ConNF.Params] (ξ : ConNF.BaseNLAction) : Set ConNF.Atom

Equations

• ξ.allOuterAtoms = ⋃ (L : ConNF.Litter), ⋃ (_ : ξ.LitterPresent L), ξ.outerAtoms L

theorem ConNF.BaseNLAction.mem_innerAtoms_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} (L : ConNF.Litter) (hL : ξ.LitterPresent L) (a : ConNF.Atom) : a ∈ ξ.innerAtoms L ↔ a.1 ≠ L ∧ ∀ (N : ConNF.NearLitter), (ξ.nearLitterMap N).Dom ∧ N.fst = L → a ∈ N

@[simp]

theorem ConNF.BaseNLAction.mem_outerAtoms_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} (L : ConNF.Litter) (a : ConNF.Atom) : a ∈ ξ.outerAtoms L ↔ a.1 = L ∧ ∀ (N : ConNF.NearLitter), (ξ.nearLitterMap N).Dom → a ∉ N

@[simp]

theorem ConNF.BaseNLAction.mem_allOuterAtoms_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} (a : ConNF.Atom) : a ∈ ξ.allOuterAtoms ↔ ξ.LitterPresent a.1 ∧ ∀ (N : ConNF.NearLitter), (ξ.nearLitterMap N).Dom → a ∉ N

theorem ConNF.BaseNLAction.litterPresent_small [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Small {L : ConNF.Litter | ξ.LitterPresent L}

theorem ConNF.BaseNLAction.litterPresent_small' [ConNF.Params] (ξ : ConNF.BaseNLAction) : ConNF.Small {N : ConNF.NearLitter | N.IsLitter ∧ ∃ (N' : ConNF.NearLitter), (ξ.nearLitterMap N').Dom ∧ N'.fst = N.fst}

theorem ConNF.BaseNLAction.innerAtoms_small [ConNF.Params] {ξ : ConNF.BaseNLAction} (L : ConNF.Litter) (hL : ξ.LitterPresent L) : ConNF.Small (ξ.innerAtoms L)

theorem ConNF.BaseNLAction.outerAtoms_small [ConNF.Params] {ξ : ConNF.BaseNLAction} (L : ConNF.Litter) (hL : ξ.LitterPresent L) : ConNF.Small (ξ.outerAtoms L)

theorem ConNF.BaseNLAction.allOuterAtoms_small [ConNF.Params] {ξ : ConNF.BaseNLAction} : ConNF.Small ξ.allOuterAtoms

def ConNF.BaseNLAction.innerAtomsCod [ConNF.Params] (ξ : ConNF.BaseNLAction) (L : ConNF.Litter) : Set ConNF.Atom

The codomain for the inner atoms.

Equations

• ξ.innerAtomsCod L = (⋂ (N : ConNF.NearLitter), ⋂ (hN : (ξ.nearLitterMap N).Dom ∧ N.fst = L), ↑((ξ.nearLitterMap N).get ⋯)) \ ξ.atomMap.ran

@[simp]

theorem ConNF.BaseNLAction.mem_innerAtomsCod_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} (L : ConNF.Litter) (a : ConNF.Atom) : a ∈ ξ.innerAtomsCod L ↔ (∀ (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom ∧ N.fst = L), a ∈ (ξ.nearLitterMap N).get ⋯) ∧ a ∉ ξ.atomMap.ran

theorem ConNF.BaseNLAction.innerAtomsCod_subset [ConNF.Params] (ξ : ConNF.BaseNLAction) (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) : ξ.innerAtomsCod N.fst ⊆ ↑((ξ.nearLitterMap N).get hN)

theorem ConNF.BaseNLAction.innerAtomsCod_eq [ConNF.Params] {ξ : ConNF.BaseNLAction} (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) : ξ.innerAtomsCod N.fst = ↑((ξ.nearLitterMap N).get hN) \ ((⋃ (N' : ConNF.NearLitter), ⋃ (hN' : (ξ.nearLitterMap N').Dom ∧ N'.fst = N.fst), symmDiff ↑((ξ.nearLitterMap N').get ⋯) ↑((ξ.nearLitterMap N).get hN)) ∪ ξ.atomMap.ran)

theorem ConNF.BaseNLAction.innerAtomsCod_eq_aux [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) : ConNF.Small ((⋃ (N' : ConNF.NearLitter), ⋃ (hN' : (ξ.nearLitterMap N').Dom ∧ N'.fst = N.fst), symmDiff ↑((ξ.nearLitterMap N').get ⋯) ↑((ξ.nearLitterMap N).get hN)) ∪ ξ.atomMap.ran)

theorem ConNF.BaseNLAction.mk_innerAtomsCod [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (L : ConNF.Litter) (hL : ξ.LitterPresent L) : Cardinal.mk ↑(ξ.innerAtomsCod L) = Cardinal.mk ConNF.κ

theorem ConNF.BaseNLAction.mk_innerAtoms_lt [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (L : ConNF.Litter) (hL : ξ.LitterPresent L) : Cardinal.mk ↑(ξ.innerAtoms L) < Cardinal.mk ↑(ξ.innerAtomsCod L)

@[irreducible]

noncomputable def ConNF.BaseNLAction.innerAtomsEmbedding [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (L : ConNF.Litter) (hL : ξ.LitterPresent L) : ↑(ξ.innerAtoms L) ↪ ↑(ξ.innerAtomsCod L)

Equations

• @ConNF.BaseNLAction.innerAtomsEmbedding = ConNF.BaseNLAction.wrapped✝.1

theorem ConNF.BaseNLAction.innerAtomsEmbedding_def [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (L : ConNF.Litter) (hL : ξ.LitterPresent L) : ConNF.BaseNLAction.innerAtomsEmbedding hξ L hL = ⋯.some

theorem ConNF.BaseNLAction.outerAtomsEmbedding_def [ConNF.Params] (ξ : ConNF.BaseNLAction) : ξ.outerAtomsEmbedding = ⋯.some

@[irreducible]

noncomputable def ConNF.BaseNLAction.outerAtomsEmbedding [ConNF.Params] (ξ : ConNF.BaseNLAction) : ↑ξ.allOuterAtoms ↪ ↑(ConNF.litterSet ξ.sandboxLitter)

Equations

• @ConNF.BaseNLAction.outerAtomsEmbedding = ConNF.BaseNLAction.wrapped✝.1

theorem ConNF.BaseNLAction.eq_of_mem_innerAtoms [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) (a : ConNF.Atom) (ha : ¬(ξ.atomMap a).Dom) {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} (hL₁ : ξ.LitterPresent L₁) (hL₂ : ξ.LitterPresent L₂) (ha₁ : a ∈ ξ.innerAtoms L₁) (ha₂ : a ∈ ξ.innerAtoms L₂) : L₁ = L₂

theorem ConNF.BaseNLAction.innerAtoms_allOuterAtoms [ConNF.Params] {ξ : ConNF.BaseNLAction} (a : ConNF.Atom) {L : ConNF.Litter} (hL : ξ.LitterPresent L) (ha₁ : a ∈ ξ.innerAtoms L) (ha₂ : a ∈ ξ.allOuterAtoms) : False

noncomputable def ConNF.BaseNLAction.extraAtomMap [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : ConNF.Atom →. ConNF.Atom

Equations

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

theorem ConNF.BaseNLAction.extraAtomMap_dom_small [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : ConNF.Small (ξ.extraAtomMap hξ).Dom

theorem ConNF.BaseNLAction.extraAtomMap_eq_of_dom [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} (a : ConNF.Atom) (ha : (ξ.atomMap a).Dom) : (ξ.extraAtomMap hξ a).get ⋯ = (ξ.atomMap a).get ha

theorem ConNF.BaseNLAction.extraAtomMap_eq_of_innerAtoms [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} (a : ConNF.Atom) (ha : ¬(ξ.atomMap a).Dom) (L : ConNF.Litter) (hL : ξ.LitterPresent L) (ha' : a ∈ ξ.innerAtoms L) : (ξ.extraAtomMap hξ a).get ⋯ = ↑((ConNF.BaseNLAction.innerAtomsEmbedding hξ L hL) ⟨a, ha'⟩)

theorem ConNF.BaseNLAction.extraAtomMap_eq_of_allOuterAtoms [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} (a : ConNF.Atom) (ha : ¬(ξ.atomMap a).Dom) (ha' : a ∈ ξ.allOuterAtoms) : (ξ.extraAtomMap hξ a).get ⋯ = ↑(ξ.outerAtomsEmbedding ⟨a, ha'⟩)

theorem ConNF.BaseNLAction.innerAtomsEmbedding_ne_atomMap [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {a : ConNF.Atom} (ha : (ξ.atomMap a).Dom) {L : ConNF.Litter} {hL : ξ.LitterPresent L} (b : ↑(ξ.innerAtoms L)) : (ξ.atomMap a).get ha ≠ ↑((ConNF.BaseNLAction.innerAtomsEmbedding hξ L hL) b)

theorem ConNF.BaseNLAction.outerAtomsEmbedding_ne_atomMap [ConNF.Params] {ξ : ConNF.BaseNLAction} {a : ConNF.Atom} (ha : (ξ.atomMap a).Dom) (b : ↑ξ.allOuterAtoms) : (ξ.atomMap a).get ha ≠ ↑(ξ.outerAtomsEmbedding b)

theorem ConNF.BaseNLAction.innerAtomsEmbedding_ne_outerAtomsEmbedding [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {L : ConNF.Litter} {hL : ξ.LitterPresent L} (a : ↑(ξ.innerAtoms L)) (b : ↑ξ.allOuterAtoms) : ↑((ConNF.BaseNLAction.innerAtomsEmbedding hξ L hL) a) ≠ ↑(ξ.outerAtomsEmbedding b)

theorem ConNF.BaseNLAction.innerAtomsEmbedding_disjoint [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {L₁ : ConNF.Litter} {L₂ : ConNF.Litter} {hL₁ : ξ.LitterPresent L₁} {hL₂ : ξ.LitterPresent L₂} (a₁ : ↑(ξ.innerAtoms L₁)) (a₂ : ↑(ξ.innerAtoms L₂)) (h : ↑((ConNF.BaseNLAction.innerAtomsEmbedding hξ L₁ hL₁) a₁) = ↑((ConNF.BaseNLAction.innerAtomsEmbedding hξ L₂ hL₂) a₂)) : L₁ = L₂

theorem ConNF.BaseNLAction.extraAtomMap_injective [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} ⦃a : ConNF.Atom⦄ ⦃b : ConNF.Atom⦄ (ha : (ξ.extraAtomMap hξ a).Dom) (hb : (ξ.extraAtomMap hξ b).Dom) (h : (ξ.extraAtomMap hξ a).get ha = (ξ.extraAtomMap hξ b).get hb) : a = b

theorem ConNF.BaseNLAction.mem_iff_of_mem_innerAtoms [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {a : ConNF.Atom} {L : ConNF.Litter} (hL : ξ.LitterPresent L) (ha' : ¬(ξ.atomMap a).Dom) (ha : a ∈ ξ.innerAtoms L) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) : a ∈ N ↔ N.fst = L

theorem ConNF.BaseNLAction.extraAtomMap_mem_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} ⦃a : ConNF.Atom⦄ (ha : (ξ.extraAtomMap hξ a).Dom) ⦃N : ConNF.NearLitter⦄ (hN : (ξ.nearLitterMap N).Dom) : (ξ.extraAtomMap hξ a).get ha ∈ (ξ.nearLitterMap N).get hN ↔ a ∈ N

theorem ConNF.BaseNLAction.extraAtomMap_dom_of_mem_symmDiff [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) {a : ConNF.Atom} (ha : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N) : (ξ.extraAtomMap hξ a).Dom

theorem ConNF.BaseNLAction.extraAtomMap_dom_of_mem_inter [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) {L : ConNF.Litter} (h : N.fst ≠ L) {a : ConNF.Atom} (ha₁ : a ∈ N) (ha₂ : a.1 = L) : (ξ.extraAtomMap hξ a).Dom

def ConNF.BaseNLAction.extraLitterMap' [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) : Set ConNF.Atom

Equations

• ξ.extraLitterMap' hξ N hN = symmDiff (↑((ξ.nearLitterMap N).get hN)) (⋃ (a : ConNF.Atom), ⋃ (ha : a ∈ symmDiff (ConNF.litterSet N.fst) ↑N), {(ξ.extraAtomMap hξ a).get ⋯})

theorem ConNF.BaseNLAction.extraLitterMap'_subset [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) : ξ.extraLitterMap' hξ N₁ hN₁ ⊆ ξ.extraLitterMap' hξ N₂ hN₂

theorem ConNF.BaseNLAction.extraLitterMap'_eq [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) : ξ.extraLitterMap' hξ N₁ hN₁ = ξ.extraLitterMap' hξ N₂ hN₂

theorem ConNF.BaseNLAction.extraLitterMap'_isNearLitter [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) : ConNF.IsNearLitter ((ξ.nearLitterMap N).get hN).fst (ξ.extraLitterMap' hξ N hN)

theorem ConNF.BaseNLAction.extraLitterMap'_disjoint [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst ≠ N₂.fst) (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) (a : ConNF.Atom) : a ∉ ξ.extraLitterMap' hξ N₁ hN₁ ∩ ξ.extraLitterMap' hξ N₂ hN₂

def ConNF.BaseNLAction.extraLitterMap [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) (N : ConNF.NearLitter) (hN : (ξ.nearLitterMap N).Dom) : ConNF.NearLitter

Equations

• ξ.extraLitterMap hξ N hN = ⟨((ξ.nearLitterMap N).get hN).fst, ⟨ξ.extraLitterMap' hξ N hN, ⋯⟩⟩

theorem ConNF.BaseNLAction.mem_extraLitterMap_iff [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {N : ConNF.NearLitter} {hN : (ξ.nearLitterMap N).Dom} (a : ConNF.Atom) : a ∈ ξ.extraLitterMap hξ N hN ↔ a ∈ ξ.extraLitterMap' hξ N hN

theorem ConNF.BaseNLAction.extraLitterMap_eq [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (h : N₁.fst = N₂.fst) (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) : ξ.extraLitterMap hξ N₁ hN₁ = ξ.extraLitterMap hξ N₂ hN₂

noncomputable def ConNF.BaseNLAction.withLitters [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : ConNF.BaseNLAction

Augments a near-litter action to define it on all litters near any near-litter in its domain. This allows us to create a litter action from it.

Equations

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

theorem ConNF.BaseNLAction.withLitters_nearLitterMap_of_dom [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) : ((ξ.withLitters hξ).nearLitterMap N).get ⋯ = (ξ.nearLitterMap N).get hN

theorem ConNF.BaseNLAction.withLitters_nearLitterMap_fst [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) : ((ξ.withLitters hξ).nearLitterMap N.fst.toNearLitter).get ⋯ = ξ.extraLitterMap hξ N hN

theorem ConNF.BaseNLAction.extraAtomMap_mem_iff' [ConNF.Params] {ξ : ConNF.BaseNLAction} {hξ : ξ.Lawful} {a : ConNF.Atom} (ha : (ξ.extraAtomMap hξ a).Dom) {N : ConNF.NearLitter} (hN : (ξ.nearLitterMap N).Dom) : (ξ.extraAtomMap hξ a).get ha ∈ ξ.extraLitterMap hξ N hN ↔ a.1 = N.fst

theorem ConNF.BaseNLAction.extraAtomMap_ran_of_mem_symmDiff [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) (hN : N₁.fst = N₂.fst.toNearLitter.fst) {a : ConNF.Atom} (ha : a ∈ symmDiff (↑((ξ.nearLitterMap N₁).get hN₁)) (ξ.extraLitterMap' hξ N₂ hN₂)) : a ∈ (ξ.extraAtomMap hξ).ran

theorem ConNF.BaseNLAction.extraAtomMap_ran_of_mem_inter [ConNF.Params] {ξ : ConNF.BaseNLAction} (hξ : ξ.Lawful) {N₁ : ConNF.NearLitter} {N₂ : ConNF.NearLitter} (hN₁ : (ξ.nearLitterMap N₁).Dom) (hN₂ : (ξ.nearLitterMap N₂).Dom) (hN : N₁.fst ≠ N₂.fst.toNearLitter.fst) {a : ConNF.Atom} (ha : a ∈ ↑((ξ.nearLitterMap N₁).get hN₁) ∩ ξ.extraLitterMap' hξ N₂ hN₂) : a ∈ (ξ.extraAtomMap hξ).ran

theorem ConNF.BaseNLAction.withLitters_lawful [ConNF.Params] (ξ : ConNF.BaseNLAction) (hξ : ξ.Lawful) : (ξ.withLitters hξ).Lawful