Theorems · Theorem · dynamical systems

SymbolicDynamics.FullShift.isClosed_mulForbidden

∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Inhabited A] {G : Type u_2} [inst_2 : Monoid G]
  [IsLeftCancelMul G] [DiscreteTopology A] (F : Set (SymbolicDynamics.FullShift.Pattern A G)),
  IsClosed (SymbolicDynamics.FullShift.mulForbidden F)

Avoiding a fixed family of patterns is a closed condition (in the product topology on G → A). Since each occurrence set { x | p.mulOccursInAt x v } is open (when A is discrete), its complement { x | ¬ p.mulOccursInAt x v } is closed; forbidden F is the intersection of these closed sets over p ∈ F and v ∈ G.

Defined in

Mathlib.Dynamics.SymbolicDynamics.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceInhabitedMonoidIsLeftCancelMulDiscreteTopology