separate_convex_open_set — Mathlib

English

For a convex open set s and a point x outside s, there exists f ∈ StrongDual 𝕜 E such that re f(a) < re f(x) for all a in s.

Русский

Для выпуклого открытого множества s и точки x вне s существует f ∈ StrongDual 𝕜 E так, что re f(a) < re f(x) для каждого a ∈ s.

LaTeX

$$$\exists f\in \mathrm{StrongDual}_{𝕜} E, \; \forall a\in s,\; \mathrm{re}(f(a)) < \mathrm{re}(f(x))$$$

Lean4

theorem separate_convex_open_set {s : Set E} (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E}
    (hx₀ : x₀ ∉ s) : ∃ f : StrongDual 𝕜 E, re (f x₀) = 1 ∧ ∀ x ∈ s, re (f x) < 1 :=
  by
  have := IsScalarTower.continuousSMul (M := ℝ) (α := E) 𝕜
  obtain ⟨g, hg⟩ := _root_.separate_convex_open_set hs₀ hs₁ hs₂ hx₀
  use extendTo𝕜'ₗ g
  simp only [re_extendTo𝕜'ₗ]
  exact hg

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