toInner — Mathlib

English

There is a natural inner product on the completion of E that extends the original inner product: for a,b in E viewed in the completion, ⟪a,b⟫_{Completion(E)} = ⟪a,b⟫_E.

Русский

Существует естественное скалярное произведение на дополнении пространства E, которое расширяет исходное скалярное произведение: для a,b ∈ E как элементы дополнения, ⟪a,b⟫_{Дополнение} = ⟪a,b⟫_E.

LaTeX

$$$\langle a,b\rangle_{\mathrm{Completion}(E)} = \langle a,b\rangle_E \quad (a,b\in E).$$$

Lean4

instance toInner {𝕜' E' : Type*} [TopologicalSpace 𝕜'] [UniformSpace E'] [Inner 𝕜' E'] : Inner 𝕜' (Completion E') where
  inner := curry <| (isDenseInducing_coe.prodMap isDenseInducing_coe).extend (uncurry (inner 𝕜'))

Похожие утверждения