specializingMap_iff_stableUnderSpecialization_image_singleton

English

A map f is specializing if and only if for every x, the closure of {f(x)} is contained in the image of the closure of {x}.

Русский

Отображение f специализирующее тогда и только тогда, когда для каждого x замыкание {f(x)} ⊆ образ замыкания {x}.

LaTeX

$$$\text{SpecializingMap}(f) \iff \forall x, \overline{\{f(x)\}} \subseteq f(\overline{\{x\}})$$$

Lean4

theorem specializingMap_iff_stableUnderSpecialization_image_singleton :
    SpecializingMap f ↔ ∀ x, StableUnderSpecialization (f '' closure { x }) := by
  simpa only [closure_singleton_eq_Iic] using Relation.fibration_iff_isLowerSet_image_Iic

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