geometric_hahn_banach_point_closed

English

If S is convex and closed and x is not in S, there exists f ∈ StrongDual 𝕜 E and u with Re f x > u and Re f a < u for all a ∈ S.

Русский

Если S выпукло и замкнуто и точка x не принадлежит S, то существует f ∈ StrongDual 𝕜 E и число u, такое что Re f x > u и Re f(a) < u для всех a ∈ S.

LaTeX

$$$\exists f : StrongDual 𝕜 E, \exists u \in \mathbb{R}, Re(f x) > u \land \forall a \in s, Re(f a) < u$$$

Lean4

theorem geometric_hahn_banach_point_closed (ht₁ : Convex ℝ t) (ht₂ : IsClosed t) (disj : x ∉ t) :
    ∃ (f : StrongDual 𝕜 E) (u : ℝ), re (f x) < u ∧ ∀ b ∈ t, u < re (f b) :=
  let ⟨f, _u, v, ha, hst, hb⟩ :=
    geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton ht₁ ht₂
      (disjoint_singleton_left.2 disj)
  ⟨f, v, hst.trans' <| ha x <| mem_singleton _, hb⟩

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