down_equiv_symm

Mathlib.Data.FinEnum

URI: https://scilib.ai/kg/mathlib#FinEnum.down_equiv_symm

← MathLib Explorer

English

The down of the ULifted inverse equals the inverse.

Русский

Обратный знак внутри ULift, взятый через down, равен обратному индексу.

LaTeX

$$$ ((\\\\operatorname{equiv} (\\\\alpha := \\\\mathrm{ULift} \\\\alpha)).\\\\operatorname{symm} i).\\\\down = \\\\operatorname{equiv}.\\\\operatorname{symm} i. $$$

Lean4

@[simp]
theorem down_equiv_symm : ((equiv (α := ULift α)).symm i).down = equiv.symm i :=
  rfl

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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