English
The map (a,b) ↦ ⟪a,b⟫ on the completion is a continuous bilinear form.
Русский
Карта (a,b) ↦ ⟪a,b⟫ на дополнении непрерывная билинеарная форма.
LaTeX
$$$\langle \cdot, \cdot \rangle : \mathrm{Completion}(E) \times \mathrm{Completion}(E) \to \mathbb{K}$ is continuous.$$
Lean4
protected theorem continuous_inner : Continuous (uncurry (inner 𝕜 (E := Completion E))) :=
by
let inner' : E →+ E →+ 𝕜 :=
{ toFun := fun x => (innerₛₗ 𝕜 x).toAddMonoidHom
map_zero' := by ext x; exact inner_zero_left _
map_add' := fun x y => by ext z; exact inner_add_left _ _ _ }
have : Continuous fun p : E × E => inner' p.1 p.2 := continuous_inner
rw [Completion.toInner, inner, uncurry_curry _]
change
Continuous
(((isDenseInducing_toCompl E).prodMap (isDenseInducing_toCompl E)).extend fun p : E × E => inner' p.1 p.2)
exact (isDenseInducing_toCompl E).extend_Z_bilin (isDenseInducing_toCompl E) this
