coverEntropyInf_restrict_subset — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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