geometric_hahn_banach_closed_compact

English

If S is convex and closed and T is disjoint from a point x, there exists f ∈ StrongDual 𝕜 E and u such that Re f(x) > u and Re f(b) > u for all b ∈ T.

Русский

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

LaTeX

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

Lean4

theorem geometric_hahn_banach_closed_compact (hs₁ : Convex ℝ s) (hs₂ : IsClosed s) (ht₁ : Convex ℝ t)
    (ht₂ : IsCompact t) (disj : Disjoint s t) :
    ∃ (f : StrongDual 𝕜 E) (u v : ℝ), (∀ a ∈ s, re (f a) < u) ∧ u < v ∧ ∀ b ∈ t, v < re (f b) :=
  let ⟨f, s, t, hs, st, ht⟩ := geometric_hahn_banach_compact_closed ht₁ ht₂ hs₁ hs₂ disj.symm
  ⟨-f, -t, -s, by simpa using ht, by simpa using st, by simpa using hs⟩

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