instCompScheme

Mathlib.AlgebraicGeometry.Morphisms.Proper

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsProper.instCompScheme

English

If f: X → Y and g: Y → Z are IsProper morphisms, then the composition f ≫ g is IsProper.

Русский

Если f: X → Y и g: Y → Z — предморфизмы, то композиция f ≫ g — IsProper.

LaTeX

$$$[IsProper(f)] \land [IsProper(g)] \Rightarrow IsProper(f \gg g)$$$

Lean4

instance [IsProper f] [IsProper g] : IsProper (f ≫ g) where

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

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

Разделы

Аффилиация

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