uniqueSigma_apply — Mathlib

English

The forward map of uniqueSigma sends (i,b) to the appropriate element of β(i) transported to β(default).

Русский

Прямое отображение uniqueSigma отправляет (i,b) в соответствующий элемент β(i), перенесенный в β(default).

LaTeX

$$$$ \\mathrm{uniqueSigma}_{\\alpha,\\beta}(i,b) = (\\mathrm{Unique.eq\\_default}(i)).rec(b). $$$$

Lean4

theorem uniqueSigma_apply {α} {β : α → Type*} [Unique α] (x : (a : α) × β a) :
    uniqueSigma β x = (Unique.eq_default _).rec x.2 :=
  rfl

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