isSmooth_comp — Mathlib

English

If f and g are smooth, then their composition f ≫ g is smooth.

Русский

Если морфизмы f и g гладкие, то их композиция гладкая.

LaTeX

$$$\text{IsSmooth}(f) \land \text{IsSmooth}(g) \Rightarrow \text{IsSmooth}(f \circ g)$$$

Lean4

/-- The composition of smooth morphisms is smooth. -/
instance isSmooth_comp {Z : Scheme.{u}} (g : Y ⟶ Z) [IsSmooth f] [IsSmooth g] : IsSmooth (f ≫ g) :=
  MorphismProperty.comp_mem _ f g ‹IsSmooth f› ‹IsSmooth g›

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