specializingMap_iff_closure_singleton_subset

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 specializing тогда и только тогда, когда для каждого x замыкание {f(x)} содержится в образе замыкания {x}.

LaTeX

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

Lean4

theorem specializingMap_iff_closure_singleton_subset : SpecializingMap f ↔ ∀ x, closure {f x} ⊆ f '' closure { x } := by
  simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]; rfl

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