LocallyConvexSpace.ofBases
theorem LocallyConvexSpace.ofBases :
∀ (𝕜 : Type u_1) (E : Type u_2) [inst : OrderedSemiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] {ι : Type u_3} (b : E → ι → Set E) (p : E → ι → Prop),
(∀ (x : E), (nhds x).HasBasis (p x) (b x)) →
(∀ (x : E) (i : ι), p x i → Convex 𝕜 (b x i)) → LocallyConvexSpace 𝕜 E
The theorem `LocallyConvexSpace.ofBases` states that for any types `𝕜` and `E`, where `𝕜` is an ordered semiring, `E` is an additive commutative monoid and a module over `𝕜`, and `E` is also a topological space, and any types `ι`, `b` as a function mapping from `E` to `ι` and yielding a set of `E`, and `p` as a function mapping from `E` to `ι` and yielding a proposition, the following holds: If every point `x` in `E` has a neighborhood filter (a collection of neighborhoods of `x`) that has a basis described by `b` and `p`, and every `b` that is true under `p` is a convex set, then the type `E` is a locally convex space over `𝕜`.
In simpler terms, if every point in our space `E` has a filter whose bases are convex sets, then `E` is a locally convex space. This theorem bridges the concepts of topological spaces, filter bases, and convexity in a mathematical structure known as a locally convex space.
More concisely: If every point in an additive commutative `𝕜`-module `E`, topological space, equipped with an ordered semiring `𝕜`, has a neighborhood filter with a convex basis, then `E` is a locally convex space over `𝕜`.
|
Disjoint.exists_open_convexes
theorem Disjoint.exists_open_convexes :
∀ {𝕜 : Type u_1} {E : Type u_2} [inst : LinearOrderedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
[inst_3 : TopologicalSpace E] [inst_4 : TopologicalAddGroup E] [inst_5 : ContinuousConstSMul 𝕜 E]
[inst_6 : LocallyConvexSpace 𝕜 E] {s t : Set E},
Disjoint s t →
Convex 𝕜 s →
IsCompact s →
Convex 𝕜 t →
IsClosed t → ∃ u v, IsOpen u ∧ IsOpen v ∧ Convex 𝕜 u ∧ Convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ Disjoint u v
The theorem states that in a locally convex space, given two disjoint convex sets `s` and `t`, where `s` is compact and `t` is closed, it is possible to find two open disjoint convex sets `u` and `v` such that `s` is contained in `u` and `t` is contained in `v`. This theorem is a variant of the separation theorem, which deals with the separation of sets in topological vector spaces.
More concisely: In a locally convex space, given disjoint compact convex set `s` and closed convex set `t`, there exist open disjoint convex sets `u` and `v` such that `s` is contained in `u` and `t` is contained in `v`.
|