Theorem: ContinuousLinearMap.copi_empty (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
inst✝ : IsEmpty ι
f : (i : ι) → M i →L[R] F
x : (i : ι) → M i
⊢ (copi f) x = 0
Tactic:
simp [copi_apply]
State after:
no goals