type_ext

Mathlib.CategoryTheory.Limits.Types.Shapes

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.PullbackCone.IsLimit.type_ext

English

If two pullback points have equal fst and snd, they are equal.

Русский

Если две точки pullback имеют равные fst и snd, то они равны.

LaTeX

$$$\\forall x,y \\in c.pt,\\; c.fst x = c.fst y \\;\\wedge\\; c.snd x = c.snd y \\Rightarrow x=y$$$

Lean4

theorem type_ext {x y : c.pt} (h₁ : c.fst x = c.fst y) (h₂ : c.snd x = c.snd y) : x = y :=
  (equivPullbackObj hc).injective (by ext <;> assumption)

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

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

Разделы

Аффилиация

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