ext

Mathlib.Data.ULift

URI: https://scilib.ai/kg/mathlib#ULift.ext

English

Two elements of ULift α are equal whenever their underlying values are equal.

Русский

Два элемента ULift α равны тогда и только тогда, когда их основания равны.

LaTeX

$$$\\forall x,y : \\mathrm{ULift}(\\alpha),\\ x.{down} = y.{down} \\Rightarrow x = y$$$

Lean4

@[ext]
theorem ext (x y : ULift α) (h : x.down = y.down) : x = y :=
  congrArg up h

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

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

Разделы

Аффилиация

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