Theorems · Theorem · dynamical systems

Dynamics.coverEntropyInfEntourage_image_le

∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) (V : SetRel Y Y),
      Dynamics.coverEntropyInfEntourage T (φ '' F) V ≤ Dynamics.coverEntropyInfEntourage S F (Prod.map φ φ ⁻¹' V)

Defined in

Mathlib.Dynamics.TopologicalEntropy.Semiconj

Cited by

1 results in Mathlib

Foundations

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