respectsIso

Mathlib.RingTheory.RingHom.OpenImmersion

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

English

IsStandardOpenImmersion respects isomorphisms.

Русский

IsStandardOpenImmersion сохраняет изоморфизмы.

LaTeX

$$$\text{IsStandardOpenImmersion respects isomorphisms}.$$$

Lean4

theorem respectsIso : RespectsIso.{u} IsStandardOpenImmersion :=
  stableUnderComposition.respectsIso fun e ↦ of_bijective e.bijective

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

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

Разделы

Аффилиация

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