stableUnderComposition — Mathlib

English

StableUnderComposition FormallyUnramified: formally unramified maps are closed under composition.

Русский

Стойкость к композиции для формально неразрывных отображений: композиция сохраняет свойство.

LaTeX

$$$$ \operatorname{StableUnderComposition}(\operatorname{FormallyUnramified}). $$$$

Lean4

theorem stableUnderComposition : StableUnderComposition FormallyUnramified :=
  by
  intro R S T _ _ _ f g _ _
  algebraize [f, g, g.comp f]
  exact .comp R S T

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