English
The entropy of the image φ''F with T equals the entropy of F with respect to the pullback uniform structure on X via φ.
Русский
Энтропия образа φ''F с T равна энтропии F относительно структуры X, полученной тяготением по φ.
LaTeX
$$$\\operatorname{coverEntropy}(T, \\phi(F)) = \\operatorname{coverEntropy}_{X}^{\\mathrm{comap}(\\phi,u)}(S, F)$$$
Lean4
/-- The entropy of `φ '' F` equals the entropy of `F` if `X` is endowed with the pullback by `φ`
of the uniform structure of `Y`. -/
theorem coverEntropy_image_of_comap (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T)
(F : Set X) : coverEntropy T (φ '' F) = @coverEntropy X (comap φ u) S F :=
by
apply le_antisymm
· refine iSup₂_le fun V V_uni ↦ (coverEntropyEntourage_image_le h F V).trans ?_
apply @coverEntropyEntourage_le_coverEntropy X (comap φ u) S F
rw [uniformity_comap φ, mem_comap]
exact ⟨V, V_uni, Subset.rfl⟩
· refine iSup₂_le fun U U_uni ↦ ?_
simp only [uniformity_comap φ, mem_comap] at U_uni
obtain ⟨V, V_uni, V_sub⟩ := U_uni
obtain ⟨W, W_uni, W_symm, W_V⟩ := comp_symm_mem_uniformity_sets V_uni
apply (coverEntropyEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
apply (le_coverEntropyEntourage_image h F W_symm).trans
exact coverEntropyEntourage_le_coverEntropy T (φ '' F) W_uni
