English
The range of a sequentially continuous function on a sequentially compact space is sequentially compact.
Русский
Образ последовательной непрерывной функции от последовательнос-но компактного пространства является последовательнос-но компактным.
LaTeX
$$$\forall X,Y [TopologicalSpace X] [TopologicalSpace Y] {f:X \to Y}, SeqContinuous f \to \forall K: Set X, IsSeqCompact K \to IsSeqCompact (Set.range f).$$$
Lean4
/-- Sequential compactness of sets is preserved under sequentially continuous functions. -/
theorem image (f_cont : SeqContinuous f) {K : Set X} (K_cpt : IsSeqCompact K) : IsSeqCompact (f '' K) :=
by
intro ys ys_in_fK
choose xs xs_in_K fxs_eq_ys using ys_in_fK
obtain ⟨a, a_in_K, phi, phi_mono, xs_phi_lim⟩ := K_cpt xs_in_K
refine ⟨f a, mem_image_of_mem f a_in_K, phi, phi_mono, ?_⟩
exact (f_cont xs_phi_lim).congr fun x ↦ fxs_eq_ys (phi x)
