Theorems · Theorem · dynamical systems

SymbolicDynamics.FullShift.mulOccursInAt_eq_cylinder

∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : Monoid G] [IsLeftCancelMul G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (g : G),
  {x | p.mulOccursInAt x g} =
    SymbolicDynamics.FullShift.cylinder (Finset.image (fun x => g * x) p.support) (p.mulShift g)

We call occurrence set for pattern p and position g the set of configurations in which a pattern p occurs at position g. This proves that it is exactly the cylinder corresponding to the pattern obtained by translating p by g. Equivalently, p.mulOccursInAt x g iff on every translated site g * w (with w ∈ p.support) the configuration x agrees with the translated pattern Pattern.mulShift p g. (This uses [IsLeftCancelMul G] to identify the preimage along left-multiplication by g.)

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

2 results in Mathlib

Foundations

Depth 79 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

InhabitedMonoidIsLeftCancelMul