instIsProperOfIsFinite

Mathlib.AlgebraicGeometry.Morphisms.Proper

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

English

As above, the finite morphism concept equals the meet of properness and affine-hom properties.

Русский

Как и выше, конечность морфизма равна пересечению свойств proper и affine-hom.

LaTeX

$$$@IsFinite = (@IsProper ⊓ @IsAffineHom)$$$

Lean4

instance (priority := 100) [IsFinite f] : IsProper f :=
  (IsFinite.iff_isProper_and_isAffineHom.mp ‹_›).1

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

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

Разделы

Аффилиация

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