instIsSmoothOfIsOpenImmersion

Mathlib.AlgebraicGeometry.Morphisms.Smooth

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsSmoothOfIsOpenImmersion

English

Open immersions are smooth (in particular, they have relative dimension 0).

Русский

Открытые вложения гладки (а значит, имеют относительную размерность 0).

LaTeX

$$If [IsOpenImmersion f], then IsSmooth f$$

Lean4

/-- Open immersions are smooth. -/
instance (priority := 900) [IsOpenImmersion f] : IsSmooth f :=
  IsSmoothOfRelativeDimension.isSmooth 0 f

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

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

Разделы

Аффилиация

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