continuous_compactOpen — Mathlib

English

A map f: X → C(Y,Z) is continuous if and only if for every compact K and every open U, the set {x | MapsTo (f x) K U} is open.

Русский

Отображение f: X → C(Y,Z) непрерывно тогда и только тогда, когда для всех компактных K и открытых U множество {x | MapsTo (f x) K U} открыто.

LaTeX

$$$ \\text{Continuous} f \\iff \\forall K\\, IsCompact K \\to \\forall U\\, IsOpen U \\to IsOpen\\{x \\mid MapsTo (f x) K U\\} $$$

Lean4

theorem continuous_compactOpen {f : X → C(Y, Z)} :
    Continuous f ↔ ∀ K, IsCompact K → ∀ U, IsOpen U → IsOpen {x | MapsTo (f x) K U} :=
  continuous_generateFrom_iff.trans forall_mem_image2

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