English
If T is continuous and F is a set covered by U, then the closure of F is covered by U ∘ V with the same index, preserving the dyn-cover relation.
Русский
Если T непрерывно и F покрывается U, то замыкание F покрыто U ∘ V с тем же индексом, сохраняя отношение dyn-cover.
LaTeX
$$$\\text{IsDynCoverOf}(T, \\mathrm{closure}(F), U \\circ V, n, s)$$$
Lean4
theorem closure (h : Continuous T) {F : Set X} {U V : Set (X × X)} (V_uni : V ∈ 𝓤 X) {n : ℕ} {s : Set X}
(s_cover : IsDynCoverOf T F U n s) : IsDynCoverOf T (closure F) (U ○ V) n s :=
by
rcases (hasBasis_symmetric.mem_iff' V).1 V_uni with ⟨W, ⟨W_uni, W_symm⟩, W_V⟩
refine IsDynCoverOf.of_entourage_subset (compRel_mono (refl U) W_V) fun x x_clos ↦ ?_
obtain ⟨y, y_x, y_F⟩ := mem_closure_iff_nhds.1 x_clos _ (ball_dynEntourage_mem_nhds h W_uni n x)
obtain ⟨z, z_s, y_z⟩ := mem_iUnion₂.1 (s_cover y_F)
refine mem_iUnion₂.2 ⟨z, z_s, ?_⟩
rw [mem_ball_symmetry (W_symm.dynEntourage T n)] at y_x
exact ball_mono (dynEntourage_comp_subset T U W n) z (mem_ball_comp y_z y_x)
