Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.Subshift.ofForbidden

{A : Type u_1} →
  [inst : TopologicalSpace A] →
    [inst_1 : Inhabited A] →
      {G : Type u_2} →
        [inst_2 : AddMonoid G] →
          [IsLeftCancelAdd G] →
            [DiscreteTopology A] →
              Set (SymbolicDynamics.FullShift.Pattern A G) → SymbolicDynamics.FullShift.Subshift A G

The subshift defined by a family of forbidden patterns F. This is a standard way to construct subshifts: Subshift.ofForbidden F consists of all configurations x : G → A in which no pattern p ∈ F occurs at any position. Formally: * the carrier is forbidden F (configurations avoiding F), * it is closed because each occurrence set is open, and * it is shift-invariant since avoidance is preserved by shifts.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceInhabitedAddMonoidIsLeftCancelAddDiscreteTopology