Theorem: ContinuousLinearMap.proj_single_apply (ForML/ContinuousLinearMap.lean)

State before:
ι : Type u_1
R : Type u_2
inst✝⁸ : Fintype ι
inst✝⁷ : DecidableEq ι
inst✝⁶ : Semiring R
M : Type u_3
inst✝⁵ : TopologicalSpace M
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
φ : ι → Type u_4
inst✝² : (i : ι) → TopologicalSpace (φ i)
inst✝¹ : (i : ι) → AddCommMonoid (φ i)
inst✝ : (i : ι) → Module R (φ i)
i : ι
x : φ i
⊢ (proj i) ((single i) x) = x
Tactic:
simp
State after:
no goals