sumArrowLequivProdArrow_symm_apply_inr

English

The map piFinTwo sends a function f to the pair (f 0, f 1).

Русский

Отображение piFinTwo отправляет функцию f в пару (f 0, f 1).

LaTeX

$$$$ (\\text{piFinTwo } R\\ M) : ((i : Fin 2) → M i) \\to M 0 × M 1 \\text{ satisfies } (f) \\mapsto (f(0), f(1)). $$$$

Lean4

@[simp]
theorem sumArrowLequivProdArrow_symm_apply_inr {α β} (f : α → M) (g : β → M) (b : β) :
    ((sumArrowLequivProdArrow α β R M).symm (f, g)) (Sum.inr b) = g b :=
  rfl

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