specializingMap_iff_closure_singleton

English

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

Русский

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

LaTeX

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

Lean4

theorem specializingMap_iff_closure_singleton (hf : Continuous f) :
    SpecializingMap f ↔ ∀ x, f '' closure { x } = closure {f x} := by
  simpa only [closure_singleton_eq_Iic] using Relation.fibration_iff_image_Iic hf.specialization_monotone

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