continuous_iff_isClosed — Mathlib

English

For a function f between topological spaces, f is continuous if and only if the preimage of every closed set is closed.

Русский

Для отображения f между топологическими пространствами непрерывность эквивалентна тому, что предобраз каждой замкнутой множества является замкнутым.

LaTeX

$$$\\operatorname{Continuous}(f) \\iff \\forall S\\subseteq Y, \\ IsClosed(S) \\to IsClosed(f^{-1}(S))$$$

Lean4

theorem continuous_iff_isClosed : Continuous f ↔ ∀ s, IsClosed s → IsClosed (f ⁻¹' s) :=
  continuous_def.trans <| compl_surjective.forall.trans <| by simp only [isOpen_compl_iff, preimage_compl]

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