Theorems · Theorem · dynamical systems

Dynamics.coverMincard_closure_le

∀ {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 → ∀ (n : ℕ), Dynamics.coverMincard T (closure F) (V.comp U) n ≤ Dynamics.coverMincard T F U n

Defined in

Mathlib.Dynamics.TopologicalEntropy.Subset

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace