Theorems · Theorem · dynamical systems

Dynamics.coverEntropyInf_eq_iSup_netEntropyInfEntourage

∀ {X : Type u_1} [inst : UniformSpace X] (T : X → X) (F : Set X),
  Dynamics.coverEntropyInf T F = ⨆ U ∈ uniformity X, Dynamics.netEntropyInfEntourage T F U

Bowen-Dinaburg's definition of topological entropy using nets is ⨆ U ∈ 𝓤 X, netEntropyEntourage T F U. This quantity is the same as the topological entropy using covers, so there is no need to define a new notion of topological entropy. This version of the theorem relates the liminf versions of topological entropy.

Defined in

Mathlib.Dynamics.TopologicalEntropy.NetEntropy

Cited by

2 results in Mathlib

Foundations

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

Assumes

UniformSpace