compactOpen_eq — Mathlib

English

The compact-open topology is defined by the equality with generateFrom of the image2 construction over compact sets and open sets.

Русский

Компактно-открытая топология задана равенством с конструкцией generateFrom над множеством image2 для компактных множеств и открытых множеств.

LaTeX

$$$ \\text{CompactOpen} = \\mathrm{generateFrom}\\bigl( \\mathrm{image2}\\,(\\lambda K U, \\{ f : C(X,Y) \\mid \\mathrm{MapsTo} f K U\\})\\;\\{K \\mid IsCompact K\\}\\;\\{U \\mid IsOpen U\\} \\bigr) $$$

Lean4

/-- Definition of `ContinuousMap.compactOpen`. -/
theorem compactOpen_eq :
    @compactOpen X Y _ _ = .generateFrom (image2 (fun K U ↦ {f | MapsTo f K U}) {K | IsCompact K} {t | IsOpen t}) :=
  rfl

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