containsIdentities

Mathlib.RingTheory.RingHom.OpenImmersion

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

English

Locally IsStandardOpenImmersion contains identities in the sense of ContainsIdentities.

Русский

Locally IsStandardOpenImmersion удовлетворяет условию ContainsIdentities.

LaTeX

$$$\operatorname{ContainsIdentities}(\text{IsStandardOpenImmersion}) = \text{Id}.$$$

Lean4

theorem containsIdentities : ContainsIdentities.{u} IsStandardOpenImmersion :=
  id

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

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

Разделы

Аффилиация

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