coverEntropy_restrict — Mathlib

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]

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