exists_rep

Mathlib.AlgebraicGeometry.RationalMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.RationalMap.exists_rep

English

For every rational map f: X.RationalMap Y there exists g: X.PartialMap Y with g.toRationalMap = f.

Русский

Для каждой рациональной карты f существует частичная карта g such that g.toRationalMap = f.

LaTeX

$$$\forall f:X.RationalMap Y\;\exists g:X.PartialMap Y, g.toRationalMap = f$$$

Lean4

theorem exists_rep (f : X ⤏ Y) : ∃ g : X.PartialMap Y, g.toRationalMap = f :=
  Quotient.exists_rep f

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

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

Разделы

Аффилиация

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