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) : dist x y + dist y z = dist x 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) : dist x y + dist y z = dist 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.