universallyClosedTypeComp — Mathlib

English

If f and g are universally closed morphisms, then their composition f ≫ g is universally closed.

Русский

Если f и g — универсально замкнутые морфизмы, то их композиция f ≫ g тоже универсально замкнута.

LaTeX

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

Lean4

instance universallyClosedTypeComp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [hf : UniversallyClosed f]
    [hg : UniversallyClosed g] : UniversallyClosed (f ≫ g) :=
  comp_mem _ _ _ hf hg

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