specializingMap_iff_isClosed_image_closure_singleton

English

Let f: X → Y be continuous. Then f is specializing if and only if for every x ∈ X, the image f(closure{ x }) is closed in Y.

Русский

Пусть f: X → Y — непрерывное отображение. Тогда f является специализирующим отображением тогда и только тогда, когда образ замыкания {x} в Y замкнут.

LaTeX

$$$\\\\text{SpecializingMap}(f) \\\\iff \\\\forall x \\in X, \\\\ IsClosed( f(\\\\overline{\\\\{x\\\\}}) ).$$$

Lean4

theorem specializingMap_iff_isClosed_image_closure_singleton (hf : Continuous f) :
    SpecializingMap f ↔ ∀ x, IsClosed (f '' closure { x }) :=
  by
  refine
    ⟨fun h x ↦ ?_, fun h ↦
      specializingMap_iff_stableUnderSpecialization_image_singleton.mpr (fun x ↦ (h x).stableUnderSpecialization)⟩
  rw [(specializingMap_iff_closure_singleton hf).mp h x]
  exact isClosed_closure

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