isStandardSmooth_stableUnderComposition

English

IsStandardSmooth is closed under composition: if f and g are standard-smooth, then g ∘ f is standard-smooth.

Русский

IsStandardSmooth замкнута относительно композиции: если f и g стандартно гладкие, то g ∘ f гладкая.

LaTeX

$$$$ \forall {R S T} [\mathrm{CommRing} R] [\mathrm{CommRing} S] [\mathrm{CommRing} T](f : R \to+* S)(g : S \to+* T), \; \operatorname{IsStandardSmooth}(f) \to \operatorname{IsStandardSmooth}(g) \to \operatorname{IsStandardSmooth}(g \circ f). $$$$

Lean4

theorem isStandardSmooth_stableUnderComposition : StableUnderComposition @IsStandardSmooth :=
  fun _ _ _ _ _ _ _ _ hf hg ↦ hg.comp hf

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