pullback_fst_of_right

Mathlib.AlgebraicGeometry.OpenImmersion

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

English

The fst projection of the pullback along the right leg is an open immersion.

Русский

Проекция fst из пуллбэка по правой ноге является открытым погружением.

LaTeX

$$IsOpenImmersion (pullback.fst g f)$$

Lean4

instance pullback_fst_of_right : IsOpenImmersion (pullback.fst g f) :=
  by
  rw [← pullbackSymmetry_hom_comp_snd]
  infer_instance

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

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

Разделы

Аффилиация

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