Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.Pattern.mulShift

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

Translate a finite pattern p so that it occurs at the translate v, before completing into a configuration. On input h : G, we proceed as follows: * if h lies in the left-translate of the support, i.e. h ∈ p.support.image (v * ·), choose (noncomputably) w ∈ p.support with v * w = h and return p.config w; * otherwise return default. This definition does not assume left-cancellation; it only chooses a preimage. Uniqueness (and the usual equations such as Pattern.mulShift p v (v * w) = p.config w) require a left-cancellation hypothesis and are proved in separate lemmas.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

4 results in Mathlib

Foundations

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

Assumes

InhabitedMonoid