uniqueProd_apply — Mathlib

English

For Lex(Prod α β) with Unique left component, the uniqueProd map sends x to the second coordinate of its underlying pair.

Русский

Для Lex(Prod α β) с уникальным левым компонентом, отображение uniqueProd отправляет x во вторую компоненту пары.

LaTeX

$$$\mathrm{uniqueProd}_{\alpha,\beta} \; x = (\mathrm{toLex}\, x).2$$$

Lean4

@[simp]
theorem uniqueProd_apply [Preorder α] [Unique α] [LE β] (x : α ×ₗ β) : uniqueProd α β x = (ofLex x).2 :=
  rfl

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