comp — Mathlib

English

If g is an immersion, then the composition f ≫ g is an immersion iff f is an immersion.

Русский

Если g — вложение, композиция f ≫ g — вложение тогда и только тогда, когда f — вложение.

LaTeX

$$$[\\text{IsImmersion}(g)] \Rightarrow ( \\text{IsImmersion}(f \\circ g) \\iff \\text{IsImmersion}(f) )$$$

Lean4

instance comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsImmersion f] [IsImmersion g] : IsImmersion (f ≫ g) :=
  MorphismProperty.IsStableUnderComposition.comp_mem f g inferInstance inferInstance

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