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