inner_coe — Mathlib

English

When a,b ∈ E are considered inside the completion, their inner product in the completion equals their original inner product in E.

Русский

Когда a и b рассматриваются как точки в дополнении, их скалярное произведение в дополнении равно оригинальному скалярному произведению в E.

LaTeX

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

Lean4

@[simp]
theorem inner_coe (a b : E) : ⟪(a : Completion E), (b : Completion E)⟫ = ⟪a, b⟫ :=
  (isDenseInducing_coe.prodMap isDenseInducing_coe).extend_eq (continuous_inner : Continuous (uncurry (inner 𝕜))) (a, b)

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