innerSL — Mathlib

English

Re-statement of norm inequality: ‖⟪x,y⟫‖ ≤ ‖x‖ · ‖y‖.

Русский

Повторное неравенство: ‖⟪x,y⟫‖ ≤ ‖x‖ · ‖y‖.

LaTeX

$$$\\\\|\\\\langle x, y \\\\rangle_A\\\\| \\\\leq \\\\|x\\\\| \\\\cdot \\\\|y\\\\|$$$

Lean4

/-- The function `⟨x, y⟩ ↦ ⟪x, y⟫` bundled as a continuous sesquilinear map. -/
noncomputable def innerSL : E →L⋆[ℂ] E →L[ℂ] A :=
  LinearMap.mkContinuous₂ (innerₛₗ : E →ₗ⋆[ℂ] E →ₗ[ℂ] A) 1 <| fun x y => by simp [innerₛₗ_apply, norm_inner_le E]

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