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.ball_eq_openSegment
{r ε : ℝ}
(hε : 0 < ε)
:
Metric.ball r ε = openSegment ℝ (r - ε) (r + ε)
Alias of the reverse direction of Real.convex_iff_isPreconnected.
Standard simplex #
theorem
stdSimplex_subset_closedBall
{ι : Type u_1}
[Fintype ι]
:
stdSimplex ℝ ι ⊆ Metric.closedBall 0 1
Every vector in stdSimplex 𝕜 ι has max-norm at most 1.
stdSimplex ℝ ι is bounded.
stdSimplex ℝ ι is closed.
stdSimplex ℝ ι is compact.
The standard one-dimensional simplex in ℝ² = Fin 2 → ℝ
is homeomorphic to the unit interval.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
stdSimplexHomeomorphUnitInterval_symm_apply_coe
(x : ↑(Set.Icc 0 1))
:
↑(stdSimplexHomeomorphUnitInterval.symm x) = ![↑x, 1 - ↑x]
@[simp]
theorem
stdSimplexHomeomorphUnitInterval_apply_coe
(f : ↑(stdSimplex ℝ (Fin 2)))
:
↑(stdSimplexHomeomorphUnitInterval f) = ↑f 0
Topological vector spaces #
theorem
segment_subset_closure_openSegment
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedRing 𝕜]
[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}
[LinearOrderedRing 𝕜]
[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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{a b : 𝕜}
(ha : 0 < a)
(hb : 0 ≤ b)
(hab : a + b = 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{a b : 𝕜}
(ha : 0 < a)
(hb : 0 ≤ b)
(hab : a + b = 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{a b : 𝕜}
(ha : 0 ≤ a)
(hb : 0 < b)
(hab : a + b = 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{a b : 𝕜}
(ha : 0 ≤ a)
(hb : 0 < b)
(hab : a + b = 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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)
:
theorem
Convex.combo_interior_self_mem_interior
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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)
:
theorem
Convex.combo_closure_interior_mem_interior
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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)
:
theorem
Convex.combo_self_interior_mem_interior
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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)
:
theorem
Convex.openSegment_interior_closure_subset_interior
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{x y : E}
(hx : x ∈ closure s)
(hy : y ∈ interior s)
{t : 𝕜}
(ht : t ∈ Set.Ioc 0 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{x y : E}
(hx : x ∈ s)
(hy : y ∈ interior s)
{t : 𝕜}
(ht : t ∈ Set.Ioc 0 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{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)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
{x y : E}
(hx : x ∈ s)
(hy : x + y ∈ interior s)
{t : 𝕜}
(ht : t ∈ Set.Ioc 0 1)
:
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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
:
In a topological vector space, the interior of a convex set is convex.
theorem
Convex.closure
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
:
In a topological vector space, the closure of a convex set is convex.
theorem
Convex.strictConvex'
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[TopologicalSpace 𝕜]
[OrderTopology 𝕜]
[ContinuousSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
(hs' : (interior s).Nonempty)
:
theorem
Convex.interior_closure_eq_interior_of_nonempty_interior
{𝕜 : Type u_2}
{E : Type u_3}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[TopologicalSpace 𝕜]
[OrderTopology 𝕜]
[ContinuousSMul 𝕜 E]
{s : Set E}
(hs : Convex 𝕜 s)
(hs' : (interior s).Nonempty)
:
theorem
convex_closed_sInter
{𝕜 : Type u_2}
{E : Type u_3}
[OrderedSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{S : Set (Set E)}
(h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s)
:
def
closedConvexHull
(𝕜 : Type u_2)
{E : Type u_3}
[OrderedSemiring 𝕜]
[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.
Equations
- closedConvexHull 𝕜 = ClosureOperator.ofCompletePred (fun (s : Set E) => Convex 𝕜 s ∧ IsClosed s) ⋯
Instances For
@[simp]
theorem
closedConvexHull_isClosed
(𝕜 : Type u_2)
{E : Type u_3}
[OrderedSemiring 𝕜]
[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}
[OrderedSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{s : Set E}
:
Convex 𝕜 ((closedConvexHull 𝕜) s)
theorem
isClosed_closedConvexHull
{𝕜 : Type u_2}
{E : Type u_3}
[OrderedSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{s : Set E}
:
IsClosed ((closedConvexHull 𝕜) s)
theorem
subset_closedConvexHull
{𝕜 : Type u_2}
{E : Type u_3}
[OrderedSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{s : Set E}
:
s ⊆ (closedConvexHull 𝕜) s
theorem
closure_subset_closedConvexHull
{𝕜 : Type u_2}
{E : Type u_3}
[OrderedSemiring 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
{s : Set E}
:
closure s ⊆ (closedConvexHull 𝕜) s
theorem
closedConvexHull_min
{𝕜 : Type u_2}
{E : Type u_3}
[OrderedSemiring 𝕜]
[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}
[OrderedSemiring 𝕜]
[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}
[OrderedSemiring 𝕜]
[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}
[LinearOrderedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousConstSMul 𝕜 E]
{s : Set E}
:
(closedConvexHull 𝕜) s = closure ((convexHull 𝕜) s)
theorem
Set.Finite.isCompact_convexHull
{E : Type u_3}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup 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}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup 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]
[TopologicalAddGroup 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]
[TopologicalAddGroup 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]
[TopologicalAddGroup 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
JoinedIn.of_segment_subset
{E : Type u_4}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[ContinuousAdd E]
[ContinuousSMul ℝ E]
{x y : E}
{s : Set E}
(h : segment ℝ x y ⊆ s)
:
JoinedIn s x y
theorem
Convex.isPathConnected
{E : Type u_3}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
{s : Set E}
(hconv : Convex ℝ s)
(hne : s.Nonempty)
:
A nonempty convex set is path connected.
theorem
Convex.isConnected
{E : Type u_3}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
{s : Set E}
(h : Convex ℝ s)
(hne : s.Nonempty)
:
A nonempty convex set is connected.
theorem
Convex.isPreconnected
{E : Type u_3}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
{s : Set E}
(h : Convex ℝ s)
:
A convex set is preconnected.
theorem
TopologicalAddGroup.pathConnectedSpace
{E : Type u_3}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
:
Every topological vector space over ℝ is path connected.
Not an instance, because it creates enormous TC subproblems (turn on pp.all).
theorem
isPathConnected_compl_of_isPathConnected_compl_zero
{E : Type u_4}
[AddCommGroup E]
[Module ℝ E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[ContinuousSMul ℝ E]
{p q : Submodule ℝ E}
(hpq : IsCompl p q)
(hpc : IsPathConnected {0}ᶜ)
:
IsPathConnected (↑q)ᶜ
Given two complementary subspaces p and q in E, if the complement of {0}
is path connected in p then the complement of q is path connected in E.