Theorems · Inductive type · dynamical systems

SymbolicDynamics.FullShift.Subshift

(A : Type u_1) → [TopologicalSpace A] → (G : Type u_2) → [AddMonoid G] → Type (max u_1 u_2)

A subshift on an alphabet A is a closed, shift-invariant subset of G → A. Formally, it is composed of: * carrier: the underlying set of allowed configurations. * isClosed: the set is topologically closed in A^G. * mapsTo: the set is invariant under all left-translation shifts (shift g).

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

5 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

TopologicalSpaceAddMonoid