up_injective

Mathlib.Data.ULift

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

English

The map ULift.up is injective.

Русский

Отображение ULift.up инъективно.

LaTeX

$$$\\forall {\\alpha \\beta} {f : \\alpha \\rightarrow \\beta}, \\operatorname{Injective}(\\mathrm{ULift}.up) $$$

Lean4

theorem up_injective : Injective (@up α) :=
  Equiv.ulift.symm.injective

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

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

Разделы

Аффилиация

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