geometric_hahn_banach_open_point — Mathlib

English

Extend the separation to the case of open convex set and a point, with real part separation in the RCLike context.

Русский

Расширяем разделение на случай открытого выпуклого множества и точки в контексте RCLike, с вещественным разделением.

LaTeX

$$$\exists f:\; \forall a\in s,\; \mathrm{re}(f(a)) < \mathrm{re}(f(x))$$$

Lean4

theorem geometric_hahn_banach_open_point (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) (disj : x ∉ s) :
    ∃ f : StrongDual 𝕜 E, ∀ a ∈ s, re (f a) < re (f x) :=
  by
  have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨f, h⟩ := _root_.geometric_hahn_banach_open_point hs₁ hs₂ disj
  use extendTo𝕜'ₗ f
  simp only [re_extendTo𝕜'ₗ]
  exact fun a a_1 ↦ h a a_1

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