eq_emptyTo

Mathlib.AlgebraicGeometry.Limits

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

English

For any f: ∅ → X, f equals the canonical emptyTo morphism.

Русский

Для любого отображения f: ∅ → X, f равен каноническому пустому отображению.

LaTeX

$$$\\forall X, f: \\emptyset \\to X,\\ f = \\mathrm{emptyTo}\,X$$$

Lean4

theorem eq_emptyTo {X : Scheme.{u}} (f : ∅ ⟶ X) : f = Scheme.emptyTo X :=
  Scheme.empty_ext f (Scheme.emptyTo X)

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

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

Разделы

Аффилиация

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