Theorems · Definition · dynamical systems

SymbolicDynamics.FullShift.cylinder

{A : Type u_1} → {G : Type u_2} → Finset G → (G → A) → Set (G → A)

A cylinder set is the set of all configurations that agree with a given reference configuration x on a fixed finite subset U of the index set G. The set U is called the support of the cylinder. Intuitively, cylinders specify the "letters" on finitely many coordinates, while leaving all other coordinates free. For example, in the full shift {0, 1}^ℤ, the cylinder determined by U = {0, 1} and x 0 = 1, x 1 = 0 consists of all bi-infinite sequences of 0s and 1s whose entries on positions 0 and 1 respectively are 1 and 0. When A has the discrete topology, cylinder sets form a basis of clopen sets for the product topology on G → A.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

6 results in Mathlib

Foundations

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