Theorems · Theorem · dynamical systems

SymbolicDynamics.FullShift.Pattern.occursInAt_shift

∀ {A : Type u_3} {G : Type u_4} [inst : Inhabited A] [inst_1 : AddMonoid G] (p : SymbolicDynamics.FullShift.Pattern A G)
  (x : G → A) (g h : G), p.occursInAt (SymbolicDynamics.FullShift.shift g x) h ↔ p.occursInAt x (g + h)

Shifting a configuration commutes with occurrences of a pattern. Formally: a pattern p occurs in the shifted configuration shift h x at position g if and only if it occurs in the original configuration x at position g + h.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedAddMonoid