instIsContPerfPairRealInnerₗOfCompleteSpace

English

For a real Hilbert space E that is complete, the inner product induces a continuous perfect pairing between E and its dual: E ≅ E*.

Русский

Для полного реального гильбертового пространства E скалярное произведение задаёт непрерывное совершенное сопряжение между E и его двойственным пространством: E ≅ E*.

LaTeX

$$innerₗ E is a continuous bijection between E and E*; i.e., E ≅ E* via x ↦ (y ↦ ⟪x,y⟫)$$

Lean4

instance [NormedAddCommGroup E] [CompleteSpace E] [InnerProductSpace ℝ E] : (innerₗ E).IsContPerfPair
    where
  continuous_uncurry := continuous_inner
  bijective_left := (toDual ℝ E).bijective
  bijective_right := by
    convert (toDual ℝ E).bijective
    ext y
    simp

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