AffineBasis.interior_convexHull
theorem AffineBasis.interior_convexHull :
∀ {ι : Type u_1} {E : Type u_2} [inst : Finite ι] [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
(b : AffineBasis ι ℝ E), interior ((convexHull ℝ) (Set.range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
The theorem `AffineBasis.interior_convexHull` states that in the context of a finite-dimensional normed real vector space, the interior of the convex hull of an affine basis is the set of all points for which the barycentric coordinates are strictly greater than zero with respect to this basis. To put it in simpler terms, if you create a convex hull using an affine basis in such a space, the points inside this hull are those that have barycentric coordinates, relative to the basis, that are all larger than zero. The theorem also notes a future goal of restating this result for affine spaces once the definition of convexity is generalized to this setting.
More concisely: In a finite-dimensional normed real vector space, the interior of the convex hull of an affine basis is the set of points with strictly positive barycentric coordinates with respect to this basis.
|
IsOpen.exists_between_affineIndependent_span_eq_top
theorem IsOpen.exists_between_affineIndependent_span_eq_top :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] {s u : Set P},
IsOpen u →
s ⊆ u →
s.Nonempty →
AffineIndependent ℝ Subtype.val →
∃ t, s ⊆ t ∧ t ⊆ u ∧ AffineIndependent ℝ Subtype.val ∧ affineSpan ℝ t = ⊤
This theorem states that for any set `s` of affine-independent points that belong to an open set `u` in a normed add-torsor `P` over a normed add-commutative group `V` with a normed space over the real numbers, there exists an extended set `t` such that `s` is a subset of `t`, `t` is a subset of `u`, `t` is also affine-independent and the affine span of `t` is the entire space. In simpler terms, from a set of non-colinear points in an open region, we can always find a larger set of points in the same region that spans the whole space while being affine-independent.
More concisely: For any open set `u` in a normed add-torsor `P` over a normed add-commutative group `V` with a normed space over the real numbers, and any affine-independent set `s` of points in `u`, there exists an affine-independent subset `t` of `u` containing `s` such that the affine span of `t` equals `P`.
|
IsOpen.affineSpan_eq_top
theorem IsOpen.affineSpan_eq_top :
∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
[inst_3 : NormedAddTorsor V P] {u : Set P}, IsOpen u → u.Nonempty → affineSpan ℝ u = ⊤
The theorem `IsOpen.affineSpan_eq_top` states that for any given nonempty open set `u` in a metric space `P` that is also a normed add-torsor over a normed add-commutative group `V` which is a normed space over the field of real numbers, the affine span of `u` is the entire space (denoted as `⊤`). In simpler terms, if we have an open set of points in a certain topological setting, the smallest affine subspace that contains all of these points is the whole space itself.
More concisely: The affine span of any nonempty open set in a metric space that is a normed add-torsor over a normed add-commutative group in a real normed space is the entire space.
|