English
The same equality as above holds; the simp lemmas describe the membership of comap/preimage in the entourages.
Русский
Та же равенство сохраняется; простые леммы описывают принадлежность компаp/предобраза окружениям.
LaTeX
$$$\\operatorname{coverEntropy}(T, \\phi(F)) = \\operatorname{coverEntropy}_{X}^{\\mathrm{comap}(\\phi,u)}(S, F) \\;\\text{(simplicity)}$$$
Lean4
/-- The entropy of `φ '' F` equals the entropy of `F` if `X` is endowed with the pullback by `φ`
of the uniform structure of `Y`. This version uses a `liminf`. -/
theorem coverEntropyInf_image_of_comap (u : UniformSpace Y) {S : X → X} {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T)
(F : Set X) : coverEntropyInf T (φ '' F) = @coverEntropyInf X (comap φ u) S F :=
by
apply le_antisymm
· refine iSup₂_le fun V V_uni ↦ (coverEntropyInfEntourage_image_le h F V).trans ?_
apply @coverEntropyInfEntourage_le_coverEntropyInf 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 (coverEntropyInfEntourage_antitone S F ((preimage_mono W_V).trans V_sub)).trans
apply (le_coverEntropyInfEntourage_image h F W_symm).trans
exact coverEntropyInfEntourage_le_coverEntropyInf T (φ '' F) W_uni
