continuous — Mathlib

English

A sequentially continuous function defined on a sequential space is continuous.

Русский

Функция, последовательностно непрерывная на последовательном пространстве, непрерывна.

LaTeX

$$$[SequentialSpace X] \Rightarrow (SeqContinuous f \Rightarrow Continuous f)$$$

Lean4

/-- A sequentially continuous function defined on a sequential space is continuous. -/
protected theorem continuous [SequentialSpace X] {f : X → Y} (hf : SeqContinuous f) : Continuous f :=
  continuous_iff_isClosed.mpr fun _s hs => (hs.isSeqClosed.preimage hf).isClosed

Похожие утверждения