forget_preservesOfLeft

Mathlib.AlgebraicGeometry.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsOpenImmersion.forget_preservesOfLeft

English

The forgetful functor forgetToTop preserves the limit of the left leg of the cospan f g.

Русский

Забывающий функтор forgetToTop сохраняет предел левой ножки коспана f g.

LaTeX

$$PreservesLimit (cospan f g) forgetToTop$$

Lean4

instance forget_preservesOfLeft : PreservesLimit (cospan f g) forget :=
  CategoryTheory.preservesLimit_of_createsLimit_and_hasLimit _ _

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

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

Разделы

Аффилиация

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