Theorems · Theorem · dynamical systems

Function.Semiconj.preimage_dynEntourage

∀ {X : Type u_1} {Y : Type u_2} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (U : Set (Y × Y)) (n : ℕ),
      Prod.map φ φ ⁻¹' Dynamics.dynEntourage T U n = Dynamics.dynEntourage S (Prod.map φ φ ⁻¹' U) n

Defined in

Mathlib.Dynamics.TopologicalEntropy.DynamicalEntourage

Cited by

2 results in Mathlib

Foundations

Depth 10 from the axioms · uses propext, Quot.sound