ulift_symm_down — Mathlib

English

Let α be any type. The inverse of the canonical equivalence between α and ULift α, when projected down, yields the identity: (Equiv.ulift.symm x).down = x for all x.

Русский

Пусть α — произвольный тип. Обратное к каноническому биекция между α и ULift α, затем понижающее отображение возвращает исходное значение: (Equiv.ulift.symm x).down = x для всех x.

LaTeX

$$$(\\mathrm{ulift}.symm\, x).down = x.$$$

Lean4

@[simp]
theorem ulift_symm_down {α} (x : α) : (Equiv.ulift.{u, v}.symm x).down = x :=
  rfl

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