comp — Mathlib

English

If f: X → Z and g: Z → Y are open immersions, then the composition f; g is an open immersion.

Русский

Пусть f: X → Z и g: Z → Y — открытые вложения; тогда композиция f ≫ g является открытым вложением.

LaTeX

$$$ (\mathrm{IsOpenImmersion}(f)) \land (\mathrm{IsOpenImmersion}(g)) \Rightarrow \mathrm{IsOpenImmersion}(f \circ g) $$$

Lean4

instance comp (g : Z ⟶ Y) [LocallyRingedSpace.IsOpenImmersion g] : LocallyRingedSpace.IsOpenImmersion (f ≫ g) :=
  PresheafedSpace.IsOpenImmersion.comp f.1 g.1

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