specializingMap — Mathlib

English

If f is a closed map, then f is a specializing map.

Русский

Если f — замкнутое отображение, тогда оно является специализирующим отображением.

LaTeX

$$$\\\\text{IsClosedMap}(f) \\\\Rightarrow \\\\text{SpecializingMap}(f).$$$

Lean4

theorem specializingMap (hf : IsClosedMap f) : SpecializingMap f :=
  specializingMap_iff_stableUnderSpecialization_image_singleton.mpr <| fun _ ↦
    (hf _ isClosed_closure).stableUnderSpecialization

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