Theorems · Theorem · dynamical systems

Dynamics.coverEntropyEntourage_closure

∀ {X : Type u_1} {T : X → X} {V : SetRel X X} [inst : UniformSpace X],
  Continuous T →
    ∀ (F : Set X) (U : SetRel X X),
      V ∈ uniformity X → Dynamics.coverEntropyEntourage T (closure F) (V.comp U) ≤ Dynamics.coverEntropyEntourage T F U

Defined in

Mathlib.Dynamics.TopologicalEntropy.Subset

Cited by

1 results in Mathlib

Foundations

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

Assumes

UniformSpace