coprod_apply — Mathlib

English

The value of f.coprod g at a point x in dom(f) × dom(g) is f(x.1) + g(x.2).

Русский

Значение f.coprod g в точке x из dom(f) × dom(g) равно f(x.1) + g(x.2).

LaTeX

$$$(f\mathrm{ coprod } g)(x) = f(\pi_1(x)) + g(\pi_2(x))$ for $x\in \operatorname{dom}(f) \times \operatorname{dom}(g)$, где $\pi_1,\pi_2$ — проекции.$$

Lean4

@[simp]
theorem coprod_apply (f : E →ₗ.[R] G) (g : F →ₗ.[R] G) (x) :
    f.coprod g x = f ⟨(x : E × F).1, x.2.1⟩ + g ⟨(x : E × F).2, x.2.2⟩ :=
  rfl

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