instSeparatingDualRealOfIsTopologicalAddGroupOfContinuousSMulOfLocallyConvexSpaceOfT1Space

English

An instance providing that Real-valued normed spaces have SeparatingDual Real E.

Русский

Инстанция, устанавливающая, что вещественные нормированные пространства обладаютSeparatingDual Real E.

LaTeX

$$⊢ SeparatingDual Real E$$

Lean4

instance {E : Type*} [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] [Module ℝ E] [ContinuousSMul ℝ E]
    [LocallyConvexSpace ℝ E] [T1Space E] : SeparatingDual ℝ E :=
  ⟨fun x hx ↦ by
    rcases geometric_hahn_banach_point_point hx.symm with ⟨f, hf⟩
    simp only [map_zero] at hf
    exact ⟨f, hf.ne'⟩⟩

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