English
Let X be a uniform space and T: X → X continuous. For any F ⊆ X, any U ⊆ X × X, and any V with V ∈ 𝓤(X), we have coverEntropyInfEntourage(T, closure(F), U ∘ V) ≤ coverEntropyInfEntourage(T, F, U).
Русский
Пусть X — равномерное пространство, T: X → X непрерывно. Для любого F ⊆ X, любого U ⊆ X × X и любого V ∈ 𝓤(X) выполняется: coverEntropyInfEntourage(T, closure(F), U ∘ V) ≤ coverEntropyInfEntourage(T, F, U).
LaTeX
$$$\operatorname{coverEntropyInfEntourage}(T, \overline{F}, U\circ V) \le \operatorname{coverEntropyInfEntourage}(T, F, U)$$$
Lean4
theorem coverEntropyInfEntourage_closure (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)}
(V_uni : V ∈ 𝓤 X) : coverEntropyInfEntourage T (closure F) (U ○ V) ≤ coverEntropyInfEntourage T F U :=
expGrowthInf_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_closure_le h F U V_uni n)
