comp — Mathlib

English

Composition of closed immersions is a closed immersion.

Русский

Произведение закрытых вложений есть закрытое вложение.

LaTeX

$$$\text{IsClosedImmersion}(f) \wedge \text{IsClosedImmersion}(g) \Rightarrow \text{IsClosedImmersion}(f \circ g)$$$

Lean4

/-- Composition of closed immersions is a closed immersion. -/
instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion f] [IsClosedImmersion g] :
    IsClosedImmersion (f ≫ g) :=
  MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

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