isLocallyClosed_range — Mathlib

English

If f: X → Y is an immersion, then the image of the underlying map is a locally closed subset of |Y|.

Русский

Если f: X → Y — вложение, образ подлежащего топологическому пространству отображается локально замкнуто в |Y|.

LaTeX

$$IsLocallyClosed(Set.range(f.base))$$

Lean4

theorem isLocallyClosed_range (f : X.Hom Y) [IsImmersion f] : IsLocallyClosed (Set.range f.base) :=
  IsImmersion.isLocallyClosed_range

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