geometric_hahn_banach_point_point

English

If CompleteSpace(ContinuousMultilinearMap 𝕜 M F) and all m_i ≠ 0, then CompleteSpace F.

Русский

Если CompleteSpace(ContinuousMultilinearMap 𝕜 M F) и все m_i ≠ 0, тогда CompleteSpace F.

LaTeX

$$$\forall i, m_i \neq 0 \Rightarrow \mathrm{CompleteSpace}(F)$$$

Lean4

/-- See also `NormedSpace.eq_iff_forall_dual_eq`. -/
theorem geometric_hahn_banach_point_point [T1Space E] (hxy : x ≠ y) : ∃ f : StrongDual ℝ E, f x < f y :=
  by
  obtain ⟨f, s, t, hs, st, ht⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton (convex_singleton y)
      isClosed_singleton (disjoint_singleton.2 hxy)
  exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩

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