continuous_inner — Mathlib

English

The map (x,y) ↦ ⟪x,y⟫ from E × E to ℝ is continuous (for a real inner product space E).

Русский

Карта (x,y) ↦ ⟪x,y⟫ из E × E в ℝ непрерывна.

LaTeX

$$$\\text{Continuous}_{E\\times E \\to \\mathbb{R}} ( (x,y) \\mapsto ⟪x,y⟫ )$$$

Lean4

theorem continuous_inner : Continuous fun p : E × E => ⟪p.1, p.2⟫ :=
  letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
  letI : IsScalarTower ℝ 𝕜 E := RestrictScalars.isScalarTower _ _ _
  isBoundedBilinearMap_inner.continuous

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