stableUnderComposition

Mathlib.RingTheory.RingHom.OpenImmersion

URI: https://scilib.ai/kg/mathlib#RingHom.IsStandardOpenImmersion.stableUnderComposition

English

Stable under Composition: the class of standard open immersions is closed under composition.

Русский

Класс стандартных открытых внедрений замкнут относительно композиции.

LaTeX

$$$\text{StableUnderComposition(IsStandardOpenImmersion)}$$$

Lean4

theorem stableUnderComposition : StableUnderComposition.{u} IsStandardOpenImmersion :=
  @comp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru