Completion of an inner product space

We show that the separation quotient and the completion of an inner product space are inner product spaces.

theorem Inseparable.inner_eq_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {x₁ x₂ y₁ y₂ : E} (hx : Inseparable x₁ x₂) (hy : Inseparable y₁ y₂) : inner 𝕜 x₁ y₁ = inner 𝕜 x₂ y₂

@[implicit_reducible]

instance SeparationQuotient.instInner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Inner 𝕜 (SeparationQuotient E)

@[simp]

theorem SeparationQuotient.inner_mk_mk {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : inner 𝕜 (mk x) (mk y) = inner 𝕜 x y

@[implicit_reducible]

instance SeparationQuotient.instInnerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 (SeparationQuotient E)

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.toInner {𝕜' : Type u_4} {E' : Type u_5} [TopologicalSpace 𝕜'] [UniformSpace E'] [Inner 𝕜' E'] : Inner 𝕜' (Completion E')

@[simp]

theorem UniformSpace.Completion.inner_coe {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] (a b : E) : inner 𝕜 ↑a ↑b = inner 𝕜 a b

theorem UniformSpace.Completion.continuous_inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : Continuous (Function.uncurry (inner 𝕜))

theorem UniformSpace.Completion.Continuous.inner {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] {α : Type u_4} [TopologicalSpace α] {f g : α → Completion E} (hf : Continuous f) (hg : Continuous g) : Continuous fun (x : α) => inner 𝕜 (f x) (g x)

@[implicit_reducible]

noncomputable instance UniformSpace.Completion.innerProductSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [InnerProductSpace 𝕜 E] : InnerProductSpace 𝕜 (Completion E)