instToImage

Mathlib.AlgebraicGeometry.Morphisms.Immersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsImmersion.instToImage

English

If f is an immersion, then the induced map f.toImage is an immersion.

Русский

Если f — вложение, то сопряженное отображение f.toImage — вложение.

LaTeX

$$$\\text{IsImmersion}(f.toImage)$$$

Lean4

instance [IsImmersion f] : IsImmersion f.toImage :=
  have : IsImmersion (f.toImage ≫ f.imageι) := by simpa
  IsImmersion.of_comp f.toImage f.imageι

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

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

Разделы

Аффилиация

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