English
Given a compact F, a maps T preserving F, and a uniform entourage U, there exists a finite s such that IsDynCoverOf T F U n s and s is mapped into F by T.
Русский
Для компактного F, отображения T сохраняющего F и окружения U существует конечное s, для которого выполняется покрытие и отображение T сохраняет s в F.
LaTeX
$$$\exists s, IsDynCoverOf T F U n s$ with $T(s) \subseteq F$$$
Lean4
theorem exists_isDynCoverOf_of_isCompact_invariant [UniformSpace X] {T : X → X} {F : Set X} (F_comp : IsCompact F)
(F_inv : MapsTo T F F) {U : Set (X × X)} (U_uni : U ∈ 𝓤 X) (n : ℕ) : ∃ s : Finset X, IsDynCoverOf T F U n s :=
by
obtain ⟨V, V_uni, V_symm, V_U⟩ := comp_symm_mem_uniformity_sets U_uni
obtain ⟨s, _, s_cover⟩ :=
IsCompact.elim_nhds_subcover F_comp (fun x : X ↦ ball x V) fun (x : X) _ ↦ ball_mem_nhds x V_uni
have : IsDynCoverOf T F V 1 s := by simp only [IsDynCoverOf, Finset.mem_coe, dynEntourage_one, s_cover]
obtain ⟨t, t_dyncover, t_card⟩ := this.iterate_le_pow F_inv V_symm n
rw [one_mul n] at t_dyncover
exact ⟨t, t_dyncover.of_entourage_subset V_U⟩
