instIsPreimmersion

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsClosedImmersion.instIsPreimmersion

English

Every closed immersion is a preimmersion.

Русский

Каждое закрытое вложение является предиммрсией.

LaTeX

$$$IsClosedImmersion f \Rightarrow IsPreimmersion f$$$

Lean4

instance (priority := 900) {X Y : Scheme} (f : X ⟶ Y) [IsClosedImmersion f] : IsPreimmersion f :=
  (iff_isPreimmersion.mp ‹_›).1

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru