orderIsoSumLexPUnit_symm_inl

Mathlib.Data.Sum.Order

URI: https://scilib.ai/kg/mathlib#WithTop.orderIsoSumLexPUnit_symm_inl

English

The symmetry of sumLexPUnit maps inr to top: (orderIsoSumLexPUnit.symm (toLex (inr a))) = top.

Русский

Симметрия sumLexPUnit отправляет inr в топ: (orderIsoSumLexPUnit.symm (toLex (inr a))) = top.

LaTeX

$$$\\bigl(\\text{orderIsoSumLexPUnit}^{-1}(\\mathrm{toLex}(\\mathrm{inr}(a)))\\bigr) = \\mathrm{top}$$$

Lean4

@[simp]
theorem orderIsoSumLexPUnit_symm_inl (a : α) : orderIsoSumLexPUnit.symm (toLex <| inl a) = a :=
  rfl

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

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

Разделы

Аффилиация

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