Convex.contractibleSpace
theorem Convex.contractibleSpace :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E] {s : Set E},
Convex ℝ s → s.Nonempty → ContractibleSpace ↑s
The theorem `Convex.contractibleSpace` states that for any real vector space `E` with a continuous addition operation, a continuous scalar multiplication operation, and a topology, any non-empty convex set `s` in `E` is a contractible space. In other words, given a type `E` equipped with the structure of a real vector space, a topological space, continuous addition and scalar multiplication, if we have a set `s` of elements from `E` such that `s` is convex and non-empty, then `s` is a contractible space. Here, a space is contractible if it is homotopic to a single point, and a set in a vector space is convex if for any two points in the set, the entire line segment between those points is also in the set.
More concisely: Any non-empty convex subset of a real vector space endowed with continuous operations and a topology is a contractible space.
|
StarConvex.contractibleSpace
theorem StarConvex.contractibleSpace :
∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
[inst_3 : ContinuousAdd E] [inst_4 : ContinuousSMul ℝ E] {s : Set E} {x : E},
StarConvex ℝ x s → s.Nonempty → ContractibleSpace ↑s
The theorem `StarConvex.contractibleSpace` states that for any set `s` of some type `E` - where `E` is a type equipped with an addition operation (`AddCommGroup`), a scalar multiplication (`Module ℝ E`), a topology (`TopologicalSpace`), a continuous addition operation (`ContinuousAdd`), and a continuous scalar multiplication (`ContinuousSMul ℝ E`) - if `s` is star-convex at some point `x` and `s` is non-empty, then `s` is a contractible space.
In mathematical terms, this means that a non-empty set, which is star-convex at a given point (that is, every line segment from this point to any other point in the set lies entirely within the set), is a contractible space (a topological space that can be continuously shrinked to a point). This applies to sets in a space where we can add elements together, multiply them by real numbers, and have a notion of closeness (topology), and where these operations are continuous.
More concisely: A non-empty, star-convex set in a topological AddCommGroup with continuous addition and scalar multiplication is a contractible space.
|