English
The entropy of restricting a map to an invariant set matches the original entropy on the restricted domain.
Русский
Энтропия ограничения отображения к инвариантному множеству совпадает с исходной энтропией на ограниченной области.
LaTeX
$$$\\operatorname{coverEntropy\\_restrict}(\\text{MapsTo }T\\,F\\,F\\,h) = \\operatorname{coverEntropy}(T, F)$$$
Lean4
/-- The entropy of the restriction of `T` to an invariant set `F` is `coverEntropy S F`. This
theorem justifies our definition of `coverEntropy T F`. -/
theorem coverEntropy_restrict [UniformSpace X] {T : X → X} {F : Set X} (h : MapsTo T F F) :
coverEntropy (h.restrict T F F) univ = coverEntropy T F := by
rw [← coverEntropy_restrict_subset Subset.rfl h, coe_preimage_self F]