sumArrowLequivProdArrow_apply_snd

English

The symm inverse maps (f,g) to a function on α ⊕ β whose values on inl and inr are f and g respectively.

Русский

Обратное отображение симметрично отображает пару (f,g) в функцию на α ⊕ β, принимающую значения f на inl и g на inr.

LaTeX

$$$$ (\\text{sumArrowLequivProdArrow }\\alpha\\beta\\,R\\,M)^{\\!\\mathrm{symm}} (f,g) \\; (\\text{inl } a) = f(a), \\quad (\\text{inr } b) = g(b). $$$$

Lean4

@[simp]
theorem sumArrowLequivProdArrow_apply_snd {α β} (f : α ⊕ β → M) (b : β) :
    (sumArrowLequivProdArrow α β R M f).2 b = f (Sum.inr b) :=
  rfl

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