Topological properties of convex sets

We prove the following facts:

• Convex.interior : interior of a convex set is convex;
• Convex.closure : closure of a convex set is convex;
• closedConvexHull_closure_eq_closedConvexHull : the closed convex hull of the closure of a set is equal to the closed convex hull of the set;
• Set.Finite.isCompact_convexHull : convex hull of a finite set is compact;
• Set.Finite.isClosed_convexHull : convex hull of a finite set is closed.

theorem Real.closedBall_eq_segment {r ε : ℝ} (hε : 0 ≤ ε) : Metric.closedBall r ε = segment ℝ (r - ε) (r + ε)

theorem Real.ball_eq_openSegment {r ε : ℝ} (hε : 0 < ε) : Metric.ball r ε = openSegment ℝ (r - ε) (r + ε)

theorem Real.convex_iff_isPreconnected {s : Set ℝ} : Convex ℝ s ↔ IsPreconnected s

theorem IsPreconnected.convex {s : Set ℝ} : IsPreconnected s → Convex ℝ s

Alias of the reverse direction of Real.convex_iff_isPreconnected.

Topological vector spaces

theorem segment_subset_closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DenselyOrdered 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {x y : E} : segment 𝕜 x y ⊆ closure (openSegment 𝕜 x y)

@[simp]

theorem closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [Ring 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [DenselyOrdered 𝕜] [PseudoMetricSpace 𝕜] [OrderTopology 𝕜] [ProperSpace 𝕜] [CompactIccSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [T2Space E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] (x y : E) : closure (openSegment 𝕜 x y) = segment 𝕜 x y

theorem Convex.combo_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • interior s + b • closure s ⊆ interior s

If s is a convex set, then a • interior s + b • closure s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also Convex.combo_interior_self_subset_interior for a weaker version.

theorem Convex.combo_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • interior s + b • s ⊆ interior s

If s is a convex set, then a • interior s + b • s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also Convex.combo_interior_closure_subset_interior for a stronger version.

theorem Convex.combo_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • closure s + b • interior s ⊆ interior s

If s is a convex set, then a • closure s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also Convex.combo_self_interior_subset_interior for a weaker version.

theorem Convex.combo_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • s + b • interior s ⊆ interior s

If s is a convex set, then a • s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also Convex.combo_closure_interior_subset_interior for a stronger version.

theorem Convex.combo_interior_closure_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ∈ interior s

theorem Convex.combo_interior_self_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) {a b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ∈ interior s

theorem Convex.combo_closure_interior_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • x + b • y ∈ interior s

theorem Convex.combo_self_interior_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {a b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) : a • x + b • y ∈ interior s

theorem Convex.openSegment_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) : openSegment 𝕜 x y ⊆ interior s

theorem Convex.openSegment_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ interior s

theorem Convex.openSegment_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) : openSegment 𝕜 x y ⊆ interior s

theorem Convex.openSegment_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) : openSegment 𝕜 x y ⊆ interior s

theorem Convex.add_smul_sub_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddRightMono 𝕜] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) : x + t • (y - x) ∈ interior s

If x ∈ closure s and y ∈ interior s, then the segment (x, y] is included in interior s.

theorem Convex.add_smul_sub_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddRightMono 𝕜] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) : x + t • (y - x) ∈ interior s

If x ∈ s and y ∈ interior s, then the segment (x, y] is included in interior s.

theorem Convex.add_smul_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddRightMono 𝕜] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) : x + t • y ∈ interior s

If x ∈ closure s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

theorem Convex.add_smul_mem_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [AddRightMono 𝕜] {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) : x + t • y ∈ interior s

If x ∈ s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

theorem Convex.interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] [ZeroLEOneClass 𝕜] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (interior s)

In a topological vector space, the interior of a convex set is convex.

theorem Convex.closure {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (closure s)

In a topological vector space, the closure of a convex set is convex.

theorem Convex.strictConvex' {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h : (s \ interior s).Pairwise fun (x y : E) => ∃ (c : 𝕜), (AffineMap.lineMap x y) c ∈ interior s) : StrictConvex 𝕜 s

A convex set s is strictly convex provided that for any two distinct points of s \ interior s, the line passing through these points has nonempty intersection with interior s.

theorem Convex.strictConvex {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h : (s \ interior s).Pairwise fun (x y : E) => (segment 𝕜 x y \ frontier s).Nonempty) : StrictConvex 𝕜 s

A convex set s is strictly convex provided that for any two distinct points x, y of s \ interior s, the segment with endpoints x, y has nonempty intersection with interior s.

theorem Convex.closure_interior_eq_closure_of_nonempty_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (hs' : (interior s).Nonempty) : closure (interior s) = closure s

theorem Convex.interior_closure_eq_interior_of_nonempty_interior {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [ContinuousSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (hs' : (interior s).Nonempty) : interior (closure s) = interior s

theorem convex_closed_sInter {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s) : Convex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)

def closedConvexHull (𝕜 : Type u_2) {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] : ClosureOperator (Set E)

The convex closed hull of a set s is the minimal convex closed set that includes s.

@[simp]

theorem closedConvexHull_isClosed (𝕜 : Type u_2) {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] (s : Set E) : (closedConvexHull 𝕜).IsClosed s = (Convex 𝕜 s ∧ IsClosed s)

theorem convex_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : Convex 𝕜 ((closedConvexHull 𝕜) s)

theorem isClosed_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : IsClosed ((closedConvexHull 𝕜) s)

theorem subset_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : s ⊆ (closedConvexHull 𝕜) s

theorem closure_subset_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : closure s ⊆ (closedConvexHull 𝕜) s

theorem closedConvexHull_min {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s t : Set E} (hst : s ⊆ t) (h_conv : Convex 𝕜 t) (h_closed : IsClosed t) : (closedConvexHull 𝕜) s ⊆ t

theorem convexHull_subset_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : (convexHull 𝕜) s ⊆ (closedConvexHull 𝕜) s

@[simp]

theorem closedConvexHull_closure_eq_closedConvexHull {𝕜 : Type u_2} {E : Type u_3} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {s : Set E} : (closedConvexHull 𝕜) (closure s) = (closedConvexHull 𝕜) s

theorem closedConvexHull_eq_closure_convexHull {𝕜 : Type u_2} {E : Type u_3} [Field 𝕜] [PartialOrder 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} : (closedConvexHull 𝕜) s = closure ((convexHull 𝕜) s)

theorem Set.Finite.isCompact_convexHull {E : Type u_3} (𝕜 : Type u_4) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : s.Finite) : IsCompact ((convexHull 𝕜) s)

Convex hull of a finite set is compact.

theorem Set.Finite.isClosed_convexHull {E : Type u_3} (𝕜 : Type u_4) [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [T2Space E] {s : Set E} (hs : s.Finite) : IsClosed ((convexHull 𝕜) s)

Convex hull of a finite set is closed.

theorem Convex.closure_subset_image_homothety_interior_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : closure s ⊆ ⇑(AffineMap.homothety x t) '' interior s

If we dilate the interior of a convex set about a point in its interior by a scale t > 1, the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

theorem Convex.closure_subset_interior_image_homothety_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)

If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

theorem Convex.subset_interior_image_homothety_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : s ⊆ interior (⇑(AffineMap.homothety x t) '' s)

If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

theorem Convex.nontrivial_iff_nonempty_interior {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) : s.Nontrivial ↔ (interior s).Nonempty

theorem Convex.Ioo_subset_of_mem_closure {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a b : 𝕜} (has : a ∈ closure s) (hbs : b ∈ closure s) : Set.Ioo a b ⊆ s

theorem Convex.nhdsWithin_inter_Iio_eq_nhdsLT {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a : 𝕜} (has : a ∈ closure s) (h' : (s ∩ Set.Iio a).Nonempty) : nhdsWithin a (s ∩ Set.Iio a) = nhdsWithin a (Set.Iio a)

theorem Convex.nhdsWithin_inter_Ioi_eq_nhdsGT {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a : 𝕜} (has : a ∈ closure s) (h' : (s ∩ Set.Ioi a).Nonempty) : nhdsWithin a (s ∩ Set.Ioi a) = nhdsWithin a (Set.Ioi a)

theorem Convex.nhdsWithin_diff_eq_nhdsNE {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a : 𝕜} (has : a ∈ closure s) (h_Iio : (s ∩ Set.Iio a).Nonempty) (h_Ioi : (s ∩ Set.Ioi a).Nonempty) : nhdsWithin a (s \ {a}) = nhdsWithin a {a}ᶜ

theorem Convex.nhdsWithin_diff_eq_nhdsLT {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a : 𝕜} (has : a ∈ closure s) (h_Iio : (s ∩ Set.Iio a).Nonempty) (h_Ioi : s ∩ Set.Ioi a = ∅) : nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Iio a)

theorem Convex.nhdsWithin_diff_eq_nhdsGT {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) {a : 𝕜} (has : a ∈ closure s) (h_Iio : s ∩ Set.Iio a = ∅) (h_Ioi : (s ∩ Set.Ioi a).Nonempty) : nhdsWithin a (s \ {a}) = nhdsWithin a (Set.Ioi a)

theorem Convex.diff_singleton_eventually_mem_nhds {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {s : Set 𝕜} (hs : Convex 𝕜 s) (a : 𝕜) : ∀ᶠ (x : 𝕜) in nhdsWithin a (s \ {a}), s \ {a} ∈ nhds x

theorem Affine.Simplex.isCompact_closedInterior {𝕜 : Type u_4} {V : Type u_5} {P : Type u_6} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module 𝕜 V] [ContinuousSMul 𝕜 V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] {n : ℕ} (s : Simplex 𝕜 P n) : IsCompact s.closedInterior

The closed interior of a simplex is compact.

theorem Affine.Simplex.isClosed_closedInterior {𝕜 : Type u_4} {V : Type u_5} {P : Type u_6} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [AddCommGroup V] [TopologicalSpace V] [IsTopologicalAddGroup V] [Module 𝕜 V] [ContinuousSMul 𝕜 V] [AddTorsor V P] [TopologicalSpace P] [IsTopologicalAddTorsor P] [T2Space P] {n : ℕ} (s : Simplex 𝕜 P n) : IsClosed s.closedInterior

The closed interior of a simplex is a closed set.