continuous_iff_seqContinuous — Mathlib

English

If the domain is a sequential space, then continuous and sequentially continuous coincide.

Русский

Если область определения является последовательным пространством, то непрерывность и последовательная непрерывность совпадают.

LaTeX

$$$[SequentialSpace X] \{f:X\to Y\} : Continuous(f) \iff SeqContinuous(f)$$$

Lean4

/-- If the domain of a function is a sequential space, then continuity of this function is
equivalent to its sequential continuity. -/
theorem continuous_iff_seqContinuous [SequentialSpace X] {f : X → Y} : Continuous f ↔ SeqContinuous f :=
  ⟨Continuous.seqContinuous, SeqContinuous.continuous⟩

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