isOpen_setOf_mapsTo — Mathlib

English

If K is compact and U is open, then the set {f ∈ C(X,Y) | MapsTo f K U} is open in the compact-open topology.

Русский

Если K компактно, а U открыто, то множество {f ∈ C(X,Y) | MapsTo f K U} открыто в компактно-открытой топологии.

LaTeX

$$$ IsOpen\\{ f : C(X,Y) \\mid MapsTo f K U\\} $ for $K$ compact and $U$ open.$$

Lean4

theorem isOpen_setOf_mapsTo (hK : IsCompact K) (hU : IsOpen U) : IsOpen {f : C(X, Y) | MapsTo f K U} :=
  isOpen_generateFrom_of_mem <| mem_image2_of_mem hK hU

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