instSeparatingDual — Mathlib

English

In a real normed space, there exists a separating dual functional.

Русский

В вещественном нормированном пространстве существует разделяющий дуальный функционал.

LaTeX

$$⊢ SeparatingDual Real E$$

Lean4

instance {E 𝕜 : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] : SeparatingDual 𝕜 E :=
  ⟨fun x hx ↦ by
    rcases exists_dual_vector 𝕜 x hx with ⟨f, -, hf⟩
    refine ⟨f, ?_⟩
    simpa [hf] using hx⟩

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