up_inj

Mathlib.Data.ULift

URI: https://scilib.ai/kg/mathlib#PLift.up_inj

English

For all x,y, up(x) = up(y) iff x = y.

Русский

Для любых x,y: x=y тогда up(x)=up(y) и наоборот.

LaTeX

$$$\\forall x,y \\in \\alpha, \\mathrm{up}(x) = \\mathrm{up}(y) \\Leftrightarrow x = y$$$

Lean4

theorem up_inj {x y : α} : up x = up y ↔ x = y := by simp

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

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

Разделы

Аффилиация

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