of_isPreimmersion — Mathlib

English

If f is a Preimmersion and its base range is closed, then f is a ClosedImmersion.

Русский

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

LaTeX

$$$[IsPreimmersion f] \land IsClosed(\mathrm{range} f_{base}) \Rightarrow IsClosedImmersion f$$$

Lean4

theorem of_isPreimmersion {X Y : Scheme} (f : X ⟶ Y) [IsPreimmersion f] (hf : IsClosed (Set.range f.base)) :
    IsClosedImmersion f :=
  iff_isPreimmersion.mpr ⟨‹_›, hf⟩

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