Simplices in normed affine spaces #
We prove the following facts:
exists_mem_interior_convexHull_affineBasis
: We can intercalate a simplex between a point and one of its neighborhoods.Convex.exists_subset_interior_convexHull_finset_of_isCompact
: We can intercalate a convex polytope between a compact convex set and one of its neighborhoods.
theorem
Wbtw.dist_add_dist
{E : Type u_1}
{P : Type u_2}
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
[PseudoMetricSpace P]
[NormedAddTorsor E P]
{x y z : P}
(h : Wbtw ℝ x y z)
:
theorem
dist_add_dist_of_mem_segment
{E : Type u_1}
[SeminormedAddCommGroup E]
[NormedSpace ℝ E]
{x y z : E}
(h : y ∈ segment ℝ x z)
:
theorem
exists_mem_interior_convexHull_affineBasis
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{s : Set E}
{x : E}
(hs : s ∈ nhds x)
:
∃ (b : AffineBasis (Fin (Module.finrank ℝ E + 1)) ℝ E),
x ∈ interior ((convexHull ℝ) (Set.range ⇑b)) ∧ (convexHull ℝ) (Set.range ⇑b) ⊆ s
We can intercalate a simplex between a point and one of its neighborhoods.
theorem
Convex.exists_subset_interior_convexHull_finset_of_isCompact
{E : Type u_1}
[NormedAddCommGroup E]
[NormedSpace ℝ E]
[FiniteDimensional ℝ E]
{s t : Set E}
(hs₁ : Convex ℝ s)
(hs₂ : IsCompact s)
(ht : t ∈ nhdsSet s)
:
∃ (u : Finset E), s ⊆ interior ((convexHull ℝ) ↑u) ∧ (convexHull ℝ) ↑u ⊆ t
We can intercalate a convex polytope between a compact convex set and one of its neighborhoods.