orderIsoPUnitSumLex_symm_inr

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#WithBot.orderIsoPUnitSumLex_symm_inr

English

The inverse of the isomorphism sends inr x to some x: orderIsoPUnitSumLex.symm (toLex (inr x)) = some x.

Русский

Обратное отображение переводит inr x в нечто равное some x.

LaTeX

$$$\\text{orderIsoPUnitSumLex.symm}(\\mathrm{toLex}(\\mathrm{inr}(x))) = \\mathrm{some}(x)$$$

Lean4

@[simp]
theorem orderIsoPUnitSumLex_symm_inr (a : α) : orderIsoPUnitSumLex.symm (toLex <| inr a) = a :=
  rfl

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

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

Разделы

Аффилиация

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