continuous_def — Mathlib

English

A function f is continuous iff the preimage of every open set is open.

Русский

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

LaTeX

$$$\mathrm{Continuous}(f) \iff \forall S, \mathrm{IsOpen}(S) \rightarrow \mathrm{IsOpen}(f^{-1}(S)).$$$

Lean4

theorem continuous_def {_ : TopologicalSpace X} {_ : TopologicalSpace Y} {f : X → Y} :
    Continuous f ↔ ∀ s, IsOpen s → IsOpen (f ⁻¹' s) :=
  ⟨fun hf => hf.1, fun h => ⟨h⟩⟩

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