toLexRelIsoLT_coe — Mathlib

English

The function part of the RelIso between Sum.Lex LT and LT on the sum is exactly the toLex map.

Русский

Функция из отношения-релизного типа между Sum.Lex LT и LT на сумме равна отображению toLex.

LaTeX

$$$\text{toLexRelIsoLT_coe} : \forall \{\alpha \beta\}, [LT\ alpha] [LT\ beta],\; \text{coe} (Sum.Lex.toLexRelIsoLT) = toLex.$$$

Lean4

@[simp]
theorem toLexRelIsoLT_coe [LT α] [LT β] : ⇑(toLexRelIsoLT (α := α) (β := β)) = toLex :=
  rfl

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