nontrivial

Mathlib.Algebra.Group.ULift

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

English

If α is a nontrivial type, then ULift α is also nontrivial.

Русский

Если α не тривиальна, то ULift α тоже не тривиальна.

LaTeX

$$$\\text{Nontrivial}(\\mathrm{ULift}\\,\\alpha) \\text{ whenever } \\text{Nontrivial}(\\alpha)$$$

Lean4

instance nontrivial [Nontrivial α] : Nontrivial (ULift α) :=
  Equiv.ulift.symm.injective.nontrivial

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

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

Разделы

Аффилиация

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