Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.Pattern.mulOccursInAt

{A : Type u_1} →
  {G : Type u_2} → [inst : Inhabited A] → [Monoid G] → SymbolicDynamics.FullShift.Pattern A G → (G → A) → G → Prop

p.mulOccursInAt x g means that the finite pattern p appears in the configuration x at position g. Formally: for every position h in the support of p, the value of the configuration at g * h coincides with the value of p.config at h. Intuitively, if you shift the configuration x by g (using mulShift g), then on the support of p you exactly recover the pattern p. This is the basic notion of "pattern occurrence" used to define subshifts via forbidden patterns.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

6 results in Mathlib

Foundations

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

Assumes

InhabitedMonoid