Structural near-litter actions

In this file, we define structural near-litter actions, which are trees of base near-litter actions.

Main declarations

• ConNF.StructNLAction: A tree of base near-litter actions.
• ConNF.StructNLAction.Lawful, ConNF.StructNLAction.Approximates: Branchwise definitions of lawfulness and approximation.
• ConNF.StructNLAction.withLitters: Branchwise augmentation of near-litter action to define its value on all litters associated to near-litters in its domain.

@[reducible, inline]

abbrev ConNF.StructNLAction [ConNF.Params] (α : ConNF.TypeIndex) : Type u

A β-structural action is a product that assigns a base near-litter action to each β-extended index.

Equations

• ConNF.StructNLAction = ConNF.Tree ConNF.BaseNLAction

def ConNF.StructNLAction.Lawful [ConNF.Params] {β : ConNF.TypeIndex} (ξ : ConNF.StructNLAction β) : Prop

Equations

• ξ.Lawful = ∀ (A : ConNF.ExtendedIndex β), (ξ A).Lawful

def ConNF.StructNLAction.Approximates [ConNF.Params] {β : ConNF.TypeIndex} (ξ : ConNF.StructNLAction β) (π : ConNF.StructPerm β) : Prop

Equations

• ξ.Approximates π = ∀ (A : ConNF.ExtendedIndex β), (ξ A).Approximates (π A)

noncomputable def ConNF.StructNLAction.withLitters [ConNF.Params] {β : ConNF.TypeIndex} (ξ : ConNF.StructNLAction β) (hξ : ξ.Lawful) : ConNF.StructNLAction β

Equations

• ξ.withLitters hξ A = (ξ A).withLitters ⋯

theorem ConNF.StructNLAction.withLitters_lawful [ConNF.Params] {β : ConNF.TypeIndex} (ξ : ConNF.StructNLAction β) (hξ : ξ.Lawful) : (ξ.withLitters hξ).Lawful