empty_ext

Mathlib.AlgebraicGeometry.Limits

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

English

Any two morphisms from the initial object ∅ to X are equal.

Русский

Любые две морфизмы из начального объекта ∅ в X равны.

LaTeX

$$$\\forall X, \\forall f,g: \\emptyset \\to X,\\ f = g$$$

Lean4

@[ext]
theorem empty_ext {X : Scheme.{u}} (f g : ∅ ⟶ X) : f = g :=
  Scheme.Hom.ext' (Subsingleton.elim (α := ∅ ⟶ _) _ _)

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

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

Разделы

Аффилиация

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