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 coverEntropyEntourage(T, closure(F), U ∘ V) ≤ coverEntropyEntourage(T, F, U).
Русский
Пусть X — равномерное пространство, T: X → X непрерывно. Для любого F ⊆ X, любого U ⊆ X × X и любого V ∈ 𝓤(X) выполняется: coverEntropyEntourage(T, closure(F), U ∘ V) ≤ coverEntropyEntourage(T, F, U).
LaTeX
$$$\operatorname{coverEntropyEntourage}(T, \overline{F}, U\circ V) \le \operatorname{coverEntropyEntourage}(T, F, U)$$$
Lean4
theorem coverEntropyEntourage_closure (h : Continuous T) (F : Set X) (U : Set (X × X)) {V : Set (X × X)}
(V_uni : V ∈ 𝓤 X) : coverEntropyEntourage T (closure F) (U ○ V) ≤ coverEntropyEntourage T F U :=
expGrowthSup_monotone fun n ↦ ENat.toENNReal_mono (coverMincard_closure_le h F U V_uni n)
