English
Let s be a convex open neighborhood of 0 in E, and let x0 ∉ s. Then there exists a continuous linear functional f with f(x0) = 1 and f(x) < 1 for all x ∈ s.
Русский
Пусть s — выпуклое открытое окрестность 0 в E, и x0 ∉ s. Тогда существует непрерывный линейный функционал f такой, что f(x0) = 1 и f(x) < 1 для всех x ∈ s.
LaTeX
$$$\exists f\in \mathrm{StrongDual} \; E,\; f(x_0) = 1 \land \forall x\in s,\; f(x) < 1$$$
Lean4
/-- Given a set `s` which is a convex neighbourhood of `0` and a point `x₀` outside of it, there is
a continuous linear functional `f` separating `x₀` and `s`, in the sense that it sends `x₀` to 1 and
all of `s` to values strictly below `1`. -/
theorem separate_convex_open_set [TopologicalSpace E] [AddCommGroup E] [IsTopologicalAddGroup E] [Module ℝ E]
[ContinuousSMul ℝ E] {s : Set E} (hs₀ : (0 : E) ∈ s) (hs₁ : Convex ℝ s) (hs₂ : IsOpen s) {x₀ : E} (hx₀ : x₀ ∉ s) :
∃ f : StrongDual ℝ E, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1 :=
by
let f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm
have :=
exists_extension_of_le_sublinear f (gauge s) (fun c hc => gauge_smul_of_nonneg hc.le)
(gauge_add_le hs₁ <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀) ?_
· obtain ⟨φ, hφ₁, hφ₂⟩ := this
have hφ₃ : φ x₀ = 1 := by
rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁, LinearPMap.mkSpanSingleton'_apply_self]
have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx => (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_isOpen hs₂ hx)
refine ⟨⟨φ, ?_⟩, hφ₃, hφ₄⟩
refine
φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
(vadd_set_subset_iff.mpr fun x hx => ?_)
change φ (-x₀ + x) ≠ 0
rw [map_add, map_neg]
specialize hφ₄ x hx
linarith
rintro ⟨x, hx⟩
obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx
rw [LinearPMap.mkSpanSingleton'_apply]
simp only [mul_one, Algebra.id.smul_eq_mul]
obtain h | h := le_or_gt y 0
· exact h.trans (gauge_nonneg _)
· rw [gauge_smul_of_nonneg h.le, smul_eq_mul, le_mul_iff_one_le_right h]
exact one_le_gauge_of_notMem (hs₁.starConvex hs₀) (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀
