Theorems · Theorem · dynamical systems

SymbolicDynamics.FullShift.Pattern.shift_apply_add_left_of_mem

∀ {A : Type u_1} [inst : Inhabited A] {G : Type u_2} [inst_1 : AddMonoid G] [IsLeftCancelAdd G]
  (p : SymbolicDynamics.FullShift.Pattern A G) (v w : G), w ∈ p.support → p.shift v (v + w) = p.config w

On the translated support, p.shift v agrees with p.config at the preimage. More precisely, if w ∈ p.support, then at the translated site v + w, the configuration p.shift v takes the value p.config w. This uses [IsLeftCancelAdd G] to identify the unique preimage of v + w under left-translation by v.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

InhabitedAddMonoidIsLeftCancelAdd