English
If F ⊆ G and a dynamical cover exists for G, then a dynamical cover exists for F with the same entourage and index.
Русский
Если F ⊆ G и существует динамический покров для G, то существует покров и для F с теми же окружениями и индексами.
LaTeX
$$$F \\subseteq G \\implies \\text{IsDynCoverOf } T\\, G\\, U\\, n\\, s \\to \\text{IsDynCoverOf } T\\, F\\, U\\, n\\, s$$$
Lean4
theorem coverEntropy_image_le_of_uniformContinuousOn_invariant [UniformSpace X] [UniformSpace Y] {S : X → X} {T : Y → Y}
{φ : X → Y} (h : Semiconj φ S T) {F G : Set X} (h' : UniformContinuousOn φ G) (hF : F ⊆ G) (hG : MapsTo S G G) :
coverEntropy T (φ '' F) ≤ coverEntropy S F :=
by
rw [← coverEntropy_restrict_subset hF hG]
have hφ : Semiconj (G.restrict φ) (hG.restrict S G G) T :=
by
intro x
rw [G.restrict_apply, G.restrict_apply, hG.val_restrict_apply, h.eq x]
apply (coverEntropy_image_le_of_uniformContinuous hφ (uniformContinuousOn_iff_restrict.1 h') (val ⁻¹' F)).trans_eq'
rw [← image_image_val_eq_restrict_image, image_preimage_coe G F, inter_eq_right.2 hF]
