Theorems · Theorem · functional analysis

separate_convex_open_set

∀ {E : Type u_2} [inst : TopologicalSpace E] [inst_1 : AddCommGroup E] [IsTopologicalAddGroup E] [inst_3 : Module ℝ E]
  [ContinuousSMul ℝ E] {s : Set E},
  0 ∈ s → Convex ℝ s → IsOpen s → ∀ {x₀ : E}, x₀ ∉ s → ∃ f, f x₀ = 1 ∧ ∀ x ∈ s, f x < 1

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.

Defined in

Mathlib.Analysis.LocallyConvex.Separation

Cited by

2 results in Mathlib

Foundations

Depth 166 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpaceAddCommGroupIsTopologicalAddGroupModuleContinuousSMul