Theorems · Theorem · dynamical systems

Dynamics.coverEntropy_image_le_of_uniformContinuous

∀ {X : Type u_1} {Y : Type u_2} [inst : UniformSpace X] [inst_1 : UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    UniformContinuous φ → ∀ (F : Set X), Dynamics.coverEntropy T (φ '' F) ≤ Dynamics.coverEntropy S F

The entropy of φ '' F is at most the entropy of F if φ is uniformly continuous.

Defined in

Mathlib.Dynamics.TopologicalEntropy.Semiconj

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpaceUniformSpace