English
For continuous T, the entropyInf over closures equals the entropyInf over the original set: coverEntropyInf(T, closure(F)) = coverEntropyInf(T, F).
Русский
При непрерывном T инфэнтропия на замыке совпадает с инфэнтропией на исходном множестве: coverEntropyInf(T, closure(F)) = coverEntropyInf(T, F).
LaTeX
$$$\operatorname{coverEntropyInf}(T, \overline{F}) = \operatorname{coverEntropyInf}(T, F)$$$
Lean4
theorem coverEntropyInf_closure (h : Continuous T) {F : Set X} : coverEntropyInf T (closure F) = coverEntropyInf T F :=
by
refine (iSup₂_le fun U U_uni ↦ ?_).antisymm (coverEntropyInf_monotone T subset_closure)
obtain ⟨V, V_uni, V_U⟩ := comp_mem_uniformity_sets U_uni
exact
le_iSup₂_of_le V V_uni
((coverEntropyInfEntourage_antitone T (closure F) V_U).trans (coverEntropyInfEntourage_closure h F V V_uni))
