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]