English
The entropy of T restricted to F defined via liminf over entourages is the supremum of coverEntropyInfEntourage(T, F, U) over all U ∈ 𝓤(X).
Русский
Энтропия T на F, определяемая через liminf по окрестностям, равна супремуму coverEntropyInfEntourage(T, F, U) по всем U ∈ 𝓤(X).
LaTeX
$$$\operatorname{coverEntropyInf}(T,F) = \sup_{U \in \mathcal{U}(X)} \operatorname{coverEntropyInfEntourage}(T,F,U)$$$
Lean4
/-- The entropy of `T` restricted to `F`, obtained by taking the supremum
of `coverEntropyInfEntourage` over entourages. Note that this supremum is approached by taking
small entourages. This second version uses a `liminf`, and is chosen as an alternative
definition for topological entropy. -/
noncomputable def coverEntropyInf [UniformSpace X] (T : X → X) (F : Set X) :=
⨆ U ∈ 𝓤 X, coverEntropyInfEntourage T F U
