comp — Mathlib

English

The composition of two open immersions is an open immersion.

Русский

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

LaTeX

$$$\\text{If } f:X\\to Y\\text{ and } g:Y\\to Z\\text{ are open immersions, then } f\\circ g\\text{ is an open immersion.}$$$

Lean4

instance comp {X Y Z : Scheme.{u}} (f : X ⟶ Y) (g : Y ⟶ Z) [IsOpenImmersion f] [IsOpenImmersion g] :
    IsOpenImmersion (f ≫ g) :=
  LocallyRingedSpace.IsOpenImmersion.comp f.toLRSHom g.toLRSHom

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