English
The preimage of a sequentially closed set under a sequentially continuous map is sequentially closed.
Русский
Образ обратной функции последовательственно замкнутое множество сохраняет свойство последовательной замкнутости под последовательностично непрерывной отображением.
LaTeX
$$$IsSeqClosed(s) \to (hf : SeqContinuous f) \to IsSeqClosed(f^{-1}(s))$$$
Lean4
/-- The preimage of a sequentially closed set under a sequentially continuous map is sequentially
closed. -/
theorem preimage {f : X → Y} {s : Set Y} (hs : IsSeqClosed s) (hf : SeqContinuous f) : IsSeqClosed (f ⁻¹' s) :=
fun _x _p hx hp =>
hs hx
(hf hp)
-- A continuous function is sequentially continuous.
