theorem PiLp.coe_proj (p : ENNReal) {ι : Type u_1} (𝕜 : Type u_2) {E : ι → Type u_3} [Semiring 𝕜] [(i : ι) → NormedAddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] {i : ι} : ⇑(proj p E i) = fun (x : PiLp p E) => x.ofLp i

@[simp]

theorem EuclideanSpace.proj_apply {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] {i : ι} (x : EuclideanSpace 𝕜 ι) : (proj i) x = x.ofLp i

theorem ContinuousLinearMap.coe_proj' (R : Type u_1) {ι : Type u_2} [Semiring R] {φ : ι → Type u_3} [(i : ι) → TopologicalSpace (φ i)] [(i : ι) → AddCommMonoid (φ i)] [(i : ι) → Module R (φ i)] (i : ι) : ⇑(proj i) = fun (x : (i : ι) → φ i) => x i

theorem EuclideanSpace.coe_equiv_symm {ι : Type u_1} {𝕜 : Type u_2} [RCLike 𝕜] : ⇑(equiv ι 𝕜).symm = WithLp.toLp 2