coverEntropy_restrict_subset — Mathlib

English

If F ⊆ G and T maps G into itself, then restricting entropy to F via the restriction map equals the entropy on F.

Русский

Если F ⊆ G и T отображает G в себя, то энтропия после ограничения на F одинаковa энтропии на F.

LaTeX

$$$\\operatorname{coverEntropy}(\\mathrm{MapsTo.restrict}\,T\\,G\\,G\\,h_G)\n\\bigl(\\operatorname{val}^{-1}(F)\\bigr) = \\operatorname{coverEntropy}(T, F)$$$

Lean4

theorem coverEntropy_restrict_subset [UniformSpace X] {T : X → X} {F G : Set X} (hF : F ⊆ G) (hG : MapsTo T G G) :
    coverEntropy (hG.restrict T G G) (val ⁻¹' F) = coverEntropy T F := by
  rw [← coverEntropy_image_of_comap _ hG.val_restrict_apply (val ⁻¹' F), image_preimage_coe G F, inter_eq_right.2 hF]

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