English
The range of 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.image f K).$$$
Lean4
/-- The range of sequentially continuous function on a sequentially compact space is sequentially
compact. -/
theorem range [SeqCompactSpace X] (f_cont : SeqContinuous f) : IsSeqCompact (Set.range f) := by
simpa using isSeqCompact_univ.image f_cont
