coverEntropy_image_le_of_uniformContinuous

English

If φ is uniformly continuous and semiconjugates S to T, then the entropy transported by φ does not exceed the entropy on the domain.

Русский

Если φ равномерно непрерывно и образует семиконъюгатность, то энтропия после образа φ не превосходит энтропии на исходной области.

LaTeX

$$$\\operatorname{coverEntropy}(T, \\phi(F)) \\le \\operatorname{coverEntropy}(S, F)$$$

Lean4

/-- The entropy of `φ '' F` is lower than entropy of `F` if  `φ` is uniformly continuous. -/
theorem coverEntropy_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y} {φ : X → Y}
    (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) : coverEntropy T (φ '' F) ≤ coverEntropy S F :=
  by
  rw [coverEntropy_image_of_comap _ h F]
  exact coverEntropy_antitone S F (uniformContinuous_iff.1 h')

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