isClopen_setOf_mapsTo — Mathlib

English

If t is closed in Y, then the set { f ∈ C(X,Y) | MapsTo f s t } is closed in C(X,Y).

Русский

Если t замкнуто в Y, то множество { f ∈ C(X,Y) | MapsTo f s t } закрыто в C(X,Y).

LaTeX

$$$\\text{IsClosed}\\{f\\in C(X,Y) \\mid \\mathrm{MapsTo}(f,s,t)\\}$$$

Lean4

theorem isClopen_setOf_mapsTo (hK : IsCompact K) (hU : IsClopen U) : IsClopen {f : C(X, Y) | MapsTo f K U} :=
  ⟨isClosed_setOf_mapsTo hU.isClosed K, isOpen_setOf_mapsTo hK hU.isOpen⟩

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