Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.mulForbidden

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

mulForbidden F is the set of configurations that avoid every pattern in F. Formally: x ∈ mulForbidden F if and only if for every pattern p ∈ F and every monoid element g : G, the pattern p does not occur in x at position g. Intuitively, mulForbidden F is the shift space defined by declaring the finite set (or family) of patterns F to be forbidden. A configuration belongs to the subshift if and only it avoids all the forbidden patterns.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

InhabitedMonoid