coverEntropy_closure — Mathlib

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))

Похожие утверждения