English
If φ is uniformly continuous on an invariant set G and F ⊆ G, then the same entropy comparison holds for F in G.
Русский
Если φ равномерно непрерывна на инвариантном множестве G и F ⊆ G, то для F в G выполняется та же оценка энтропии.
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. This
version uses a `liminf`. -/
theorem coverEntropyInf_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) :
coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F :=
by
rw [coverEntropyInf_image_of_comap _ h F]
exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')