Theorems · Theorem · dynamical systems

Dynamics.le_coverMincard_image

∀ {X : Type u_1} {Y : Type u_2} {V : SetRel Y Y} {S : X → X} {T : Y → Y} {φ : X → Y},
  Function.Semiconj φ S T →
    ∀ (F : Set X) [V.IsSymm] (n : ℕ),
      Dynamics.coverMincard S F (Prod.map φ φ ⁻¹' V.comp V) n ≤ Dynamics.coverMincard T (φ '' F) V n

Defined in

Mathlib.Dynamics.TopologicalEntropy.Semiconj

Cited by

2 results in Mathlib

Foundations

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

Assumes

SetRel.IsSymm