Theorem: ContinuousLinearMap.coprod_eq_comp_fst_add_comp_snd (ForML/ContinuousLinearMapCo.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝¹⁰ : Fintype ι
inst✝⁹ : DecidableEq ι
inst✝⁸ : NontriviallyNormedField R
M₁ : Type u_3
M₂ : Type u_4
inst✝⁷ : NormedAddCommGroup M₁
inst✝⁶ : NormedSpace R M₁
inst✝⁵ : NormedAddCommGroup M₂
inst✝⁴ : NormedSpace R M₂
M : ι → Type u_5
inst✝³ : (i : ι) → NormedAddCommGroup (M i)
inst✝² : (i : ι) → NormedSpace R (M i)
F : Type u_6
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace R F
f : M₁ →L[R] F
g : M₂ →L[R] F
⊢ coprod f g = comp f (fst R M₁ M₂) + comp g (snd R M₁ M₂)
Tactic:
ext x <;> simp [coprod_apply, comp_apply]
State after:
no goals