doc-next-gen

Mathlib.Analysis.Convex.Topology

Module docstring

{"# 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. ","### Standard simplex ","### Topological vector spaces "}
Real.closedBall_eq_segment theorem
(hε : 0 ≤ ε) : closedBall r ε = segment ℝ (r - ε) (r + ε)
Full source 
lemma closedBall_eq_segment (hε : 0 ≤ ε) : closedBall r ε = segment ℝ (r - ε) (r + ε) := by
  rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans <| le_add_of_nonneg_right hε)]
Closed Ball in Real Numbers as Convex Segment: $\overline{B}(r, \varepsilon) = [r - \varepsilon, r + \varepsilon]$
Informal description
For any real number $r$ and any non-negative real number $\varepsilon$, the closed ball $\overline{B}(r, \varepsilon)$ in $\mathbb{R}$ is equal to the closed convex segment between $r - \varepsilon$ and $r + \varepsilon$, i.e., \[ \overline{B}(r, \varepsilon) = [r - \varepsilon, r + \varepsilon]. \]
Real.ball_eq_openSegment theorem
(hε : 0 < ε) : ball r ε = openSegment ℝ (r - ε) (r + ε)
Full source 
lemma ball_eq_openSegment (hε : 0 < ε) : ball r ε = openSegment ℝ (r - ε) (r + ε) := by
  rw [ball_eq_Ioo, openSegment_eq_Ioo ((sub_lt_self _ hε).trans <| lt_add_of_pos_right _ hε)]
Open Ball in Reals Equals Open Interval: $\text{ball}(r, \varepsilon) = (r - \varepsilon, r + \varepsilon)$
Informal description
For any real number $r$ and positive real number $\varepsilon$, the open ball $\text{ball}(r, \varepsilon)$ in $\mathbb{R}$ is equal to the open segment between $r - \varepsilon$ and $r + \varepsilon$, i.e., \[ \text{ball}(r, \varepsilon) = (r - \varepsilon, r + \varepsilon). \]
stdSimplex_subset_closedBall theorem
: stdSimplex ℝ ι ⊆ Metric.closedBall 0 1
Full source 
/-- Every vector in `stdSimplex 𝕜 ι` has `max`-norm at most `1`. -/
theorem stdSimplex_subset_closedBall : stdSimplexstdSimplex ℝ ι ⊆ Metric.closedBall 0 1 := fun f hf ↦ by
  rw [Metric.mem_closedBall, dist_pi_le_iff zero_le_one]
  intro x
  rw [Pi.zero_apply, Real.dist_0_eq_abs, abs_of_nonneg <| hf.1 x]
  exact (mem_Icc_of_mem_stdSimplex hf x).2
Standard Simplex is Contained in Unit Ball: $\text{stdSimplex}(\mathbb{R}, \iota) \subseteq \overline{B}(0, 1)$
Informal description
The standard simplex in $\mathbb{R}^\iota$, defined as the set of all vectors with non-negative coordinates that sum to 1, is contained in the closed unit ball centered at the origin. That is, $\text{stdSimplex}(\mathbb{R}, \iota) \subseteq \overline{B}(0, 1)$.
isClosed_stdSimplex theorem
: IsClosed (stdSimplex ℝ ι)
Full source 
/-- `stdSimplex ℝ ι` is closed. -/
theorem isClosed_stdSimplex : IsClosed (stdSimplex ℝ ι) :=
  (stdSimplex_eq_inter ℝ ι).symm ▸
    IsClosed.inter (isClosed_iInter fun i => isClosed_le continuous_const (continuous_apply i))
      (isClosed_eq (continuous_finset_sum _ fun x _ => continuous_apply x) continuous_const)
Closedness of the Standard Simplex in $\mathbb{R}^\iota$
Informal description
The standard simplex in $\mathbb{R}^\iota$, defined as the set of all functions $f \colon \iota \to \mathbb{R}$ with $f(x) \geq 0$ for all $x \in \iota$ and $\sum_{x \in \iota} f(x) = 1$, is a closed subset of $\mathbb{R}^\iota$ with respect to the product topology.
isCompact_stdSimplex theorem
: IsCompact (stdSimplex ℝ ι)
Full source 
/-- `stdSimplex ℝ ι` is compact. -/
theorem isCompact_stdSimplex : IsCompact (stdSimplex ℝ ι) :=
  Metric.isCompact_iff_isClosed_bounded.2 ⟨isClosed_stdSimplex ι, bounded_stdSimplex ι⟩
Compactness of the Standard Simplex in $\mathbb{R}^\iota$
Informal description
The standard simplex in $\mathbb{R}^\iota$, defined as the set of all functions $f \colon \iota \to \mathbb{R}$ with $f(x) \geq 0$ for all $x \in \iota$ and $\sum_{x \in \iota} f(x) = 1$, is compact.
stdSimplexHomeomorphUnitInterval definition
: stdSimplex ℝ (Fin 2) ≃ₜ unitInterval
Full source 
/-- The standard one-dimensional simplex in `ℝ² = Fin 2 → ℝ`
is homeomorphic to the unit interval. -/
@[simps! -fullyApplied]
def stdSimplexHomeomorphUnitInterval : stdSimplexstdSimplex ℝ (Fin 2) ≃ₜ unitInterval where
  toEquiv := stdSimplexEquivIcc ℝ
  continuous_toFun := .subtype_mk ((continuous_apply 0).comp continuous_subtype_val) _
  continuous_invFun := by
    apply Continuous.subtype_mk
    exact (continuous_pi <| Fin.forall_fin_two.2
      ⟨continuous_subtype_val, continuous_const.sub continuous_subtype_val⟩)
Homeomorphism between standard 1-simplex and unit interval
Informal description
The standard one-dimensional simplex in $\mathbb{R}^2$ (represented as functions $\text{Fin}\, 2 \to \mathbb{R}$ with non-negative values summing to 1) is homeomorphic to the unit interval $[0,1] \subseteq \mathbb{R}$. The homeomorphism is given by: - Forward direction: $f \mapsto f(0)$ (the first component) - Backward direction: $x \mapsto (x, 1-x)$ (the pair of components summing to 1)
segment_subset_closure_openSegment theorem
: [x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y)
Full source 
theorem segment_subset_closure_openSegment : [x -[𝕜] y][x -[𝕜] y] ⊆ closure (openSegment 𝕜 x y) := by
  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
  exact image_closure_subset_closure_image (by fun_prop)
Closed Segment is Contained in Closure of Open Segment
Informal description
For any two points $x$ and $y$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closed segment $[x, y]$ is contained in the closure of the open segment $(x, y)$.
closure_openSegment theorem
(x y : E) : closure (openSegment 𝕜 x y) = [x -[𝕜] y]
Full source 
@[simp]
theorem closure_openSegment (x y : E) : closure (openSegment 𝕜 x y) = [x -[𝕜] y] := by
  rw [segment_eq_image, openSegment_eq_image, ← closure_Ioo (zero_ne_one' 𝕜)]
  exact (image_closure_of_isCompact (isBounded_Ioo _ _).isCompact_closure <|
    Continuous.continuousOn <| by fun_prop).symm
Closure of Open Segment Equals Closed Segment
Informal description
For any two points $x$ and $y$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closure of the open segment $(x, y)$ is equal to the closed segment $[x, y]$.
Convex.combo_interior_closure_subset_interior theorem
{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
Full source 
/-- 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_closure_subset_interior {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 :=
  interior_smul₀ ha.ne' s ▸
    calc
      interior (a • s) + b • closure s ⊆ interior (a • s) + closure (b • s) :=
        add_subset_add Subset.rfl (smul_closure_subset b s)
      _ = interior (a • s) + b • s := by rw [isOpen_interior.add_closure (b • s)]
      _ ⊆ interior (a • s + b • s)calc
      interior (a • s) + b • closure s ⊆ interior (a • s) + closure (b • s) :=
        add_subset_add Subset.rfl (smul_closure_subset b s)
      _ = interior (a • s) + b • s := by rw [isOpen_interior.add_closure (b • s)]
      _ ⊆ interior (a • s + b • s) := subset_interior_add_left
      _ ⊆ interior s := interior_mono <| hs.set_combo_subset ha.le hb hab
Convex Combination of Interior and Closure Subset Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any scalars $a, b \in \mathbb{K}$ such that $0 < a$, $0 \leq b$, and $a + b = 1$, the combination $a \cdot \text{interior}(s) + b \cdot \text{closure}(s)$ is contained in the interior of $s$, i.e., \[ a \cdot \text{interior}(s) + b \cdot \text{closure}(s) \subseteq \text{interior}(s). \]
Convex.combo_interior_self_subset_interior theorem
{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
Full source 
/-- 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_interior_self_subset_interior {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 :=
  calc
    a • interior s + b • s ⊆ a • interior s + b • closure s :=
      add_subset_add Subset.rfl <| image_subset _ subset_closure
    _ ⊆ interior s := hs.combo_interior_closure_subset_interior ha hb hab
Convex Combination of Interior and Set Subset Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any scalars $a, b \in \mathbb{K}$ such that $0 < a$, $0 \leq b$, and $a + b = 1$, the combination $a \cdot \text{interior}(s) + b \cdot s$ is contained in the interior of $s$, i.e., \[ a \cdot \text{interior}(s) + b \cdot s \subseteq \text{interior}(s). \]
Convex.combo_closure_interior_subset_interior theorem
{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
Full source 
/-- 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_closure_interior_subset_interior {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 := by
  rw [add_comm]
  exact hs.combo_interior_closure_subset_interior hb ha (add_comm a b ▸ hab)
Convex Combination of Closure and Interior Subset Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any scalars $a, b \in \mathbb{K}$ such that $0 \leq a$, $0 < b$, and $a + b = 1$, the combination $a \cdot \text{closure}(s) + b \cdot \text{interior}(s)$ is contained in the interior of $s$, i.e., \[ a \cdot \text{closure}(s) + b \cdot \text{interior}(s) \subseteq \text{interior}(s). \]
Convex.combo_self_interior_subset_interior theorem
{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
Full source 
/-- 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_self_interior_subset_interior {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 := by
  rw [add_comm]
  exact hs.combo_interior_self_subset_interior hb ha (add_comm a b ▸ hab)
Convex Combination of Set and Interior Subset Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any scalars $a, b \in \mathbb{K}$ such that $0 \leq a$, $0 < b$, and $a + b = 1$, the combination $a \cdot s + b \cdot \text{interior}(s)$ is contained in the interior of $s$, i.e., \[ a \cdot s + b \cdot \text{interior}(s) \subseteq \text{interior}(s). \]
Convex.combo_interior_closure_mem_interior theorem
{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
Full source 
theorem Convex.combo_interior_closure_mem_interior {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 :=
  hs.combo_interior_closure_subset_interior ha hb hab <|
    add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
Convex Combination of Interior and Closure Points Lies in Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{interior}(s)$ and $y \in \text{closure}(s)$, and scalars $a, b \in \mathbb{K}$ such that $0 < a$, $0 \leq b$, and $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ lies in the interior of $s$.
Convex.combo_interior_self_mem_interior theorem
{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
Full source 
theorem Convex.combo_interior_self_mem_interior {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 :=
  hs.combo_interior_closure_mem_interior hx (subset_closure hy) ha hb hab
Convex Combination of Interior and Set Points Lies in Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{interior}(s)$ and $y \in s$, and scalars $a, b \in \mathbb{K}$ such that $0 < a$, $0 \leq b$, and $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ lies in the interior of $s$.
Convex.combo_closure_interior_mem_interior theorem
{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
Full source 
theorem Convex.combo_closure_interior_mem_interior {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 :=
  hs.combo_closure_interior_subset_interior ha hb hab <|
    add_mem_add (smul_mem_smul_set hx) (smul_mem_smul_set hy)
Convex Combination of Closure and Interior Points Lies in Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{closure}(s)$ and $y \in \text{interior}(s)$, and scalars $a, b \in \mathbb{K}$ such that $0 \leq a$, $0 < b$, and $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ lies in the interior of $s$.
Convex.combo_self_interior_mem_interior theorem
{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
Full source 
theorem Convex.combo_self_interior_mem_interior {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 :=
  hs.combo_closure_interior_mem_interior (subset_closure hx) hy ha hb hab
Convex Combination of Set and Interior Points Lies in Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in s$ and $y \in \text{interior}(s)$, and scalars $a, b \in \mathbb{K}$ such that $0 \leq a$, $0 < b$, and $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ lies in the interior of $s$.
Convex.openSegment_interior_closure_subset_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) : openSegment 𝕜 x y ⊆ interior s
Full source 
theorem Convex.openSegment_interior_closure_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ interior s) (hy : y ∈ closure s) : openSegmentopenSegment 𝕜 x y ⊆ interior s := by
  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  exact hs.combo_interior_closure_mem_interior hx hy ha hb.le hab
Open Segment Between Interior and Closure Points Lies in Interior of Convex Set
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{interior}(s)$ and $y \in \text{closure}(s)$, the open segment connecting $x$ and $y$ is entirely contained in the interior of $s$.
Convex.openSegment_interior_self_subset_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ interior s
Full source 
theorem Convex.openSegment_interior_self_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ interior s) (hy : y ∈ s) : openSegmentopenSegment 𝕜 x y ⊆ interior s :=
  hs.openSegment_interior_closure_subset_interior hx (subset_closure hy)
Open Segment Between Interior and Set Points Lies in Interior of Convex Set
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{interior}(s)$ and $y \in s$, the open segment connecting $x$ and $y$ is entirely contained in the interior of $s$.
Convex.openSegment_closure_interior_subset_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) : openSegment 𝕜 x y ⊆ interior s
Full source 
theorem Convex.openSegment_closure_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ closure s) (hy : y ∈ interior s) : openSegmentopenSegment 𝕜 x y ⊆ interior s := by
  rintro _ ⟨a, b, ha, hb, hab, rfl⟩
  exact hs.combo_closure_interior_mem_interior hx hy ha.le hb hab
Open Segment Between Closure and Interior Points Lies in Interior of Convex Set
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{closure}(s)$ and $y \in \text{interior}(s)$, the open segment connecting $x$ and $y$ is entirely contained in the interior of $s$.
Convex.openSegment_self_interior_subset_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) : openSegment 𝕜 x y ⊆ interior s
Full source 
theorem Convex.openSegment_self_interior_subset_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ s) (hy : y ∈ interior s) : openSegmentopenSegment 𝕜 x y ⊆ interior s :=
  hs.openSegment_closure_interior_subset_interior (subset_closure hx) hy
Open Segment Between Boundary and Interior Points Lies in Interior of Convex Set
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in s$ and $y \in \text{interior}(s)$, the open segment connecting $x$ and $y$ is entirely contained in the interior of $s$.
Convex.add_smul_sub_mem_interior' theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • (y - x) ∈ interior s
Full source 
/-- 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' {s : Set E} (hs : Convex 𝕜 s) {x y : E}
    (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) :
    x + t • (y - x) ∈ interior s := by
  simpa only [sub_smul, smul_sub, one_smul, add_sub, add_comm] using
    hs.combo_interior_closure_mem_interior hy hx ht.1 (sub_nonneg.mpr ht.2)
      (add_sub_cancel _ _)
Convex combination of closure and interior points lies in interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{closure}(s)$ and $y \in \text{interior}(s)$, and any scalar $t \in \mathbb{K}$ such that $0 < t \leq 1$, the point $x + t(y - x)$ lies in the interior of $s$.
Convex.add_smul_sub_mem_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • (y - x) ∈ interior s
Full source 
/-- If `x ∈ s` and `y ∈ interior s`, then the segment `(x, y]` is included in `interior s`. -/
theorem Convex.add_smul_sub_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s)
    (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • (y - x) ∈ interior s :=
  hs.add_smul_sub_mem_interior' (subset_closure hx) hy ht
Convex combination of interior and boundary points lies in interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in s$ and $y \in \text{interior}(s)$, and any scalar $t \in \mathbb{K}$ such that $0 < t \leq 1$, the point $x + t(y - x)$ lies in the interior of $s$.
Convex.add_smul_mem_interior' theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s
Full source 
/-- 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' {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ closure s)
    (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s := by
  simpa only [add_sub_cancel_left] using hs.add_smul_sub_mem_interior' hx hy ht
Convex combination of closure point and interior direction lies in interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in \text{closure}(s)$ and $y \in E$ such that $x + y \in \text{interior}(s)$, and any scalar $t \in \mathbb{K}$ with $0 < t \leq 1$, the point $x + t y$ lies in the interior of $s$.
Convex.add_smul_mem_interior theorem
{s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s
Full source 
/-- If `x ∈ s` and `x + y ∈ interior s`, then `x + t y ∈ interior s` for `t ∈ (0, 1]`. -/
theorem Convex.add_smul_mem_interior {s : Set E} (hs : Convex 𝕜 s) {x y : E} (hx : x ∈ s)
    (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Ioc (0 : 𝕜) 1) : x + t • y ∈ interior s :=
  hs.add_smul_mem_interior' (subset_closure hx) hy ht
Convex combination of interior direction lies in interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. For any points $x \in s$ and $y \in E$ such that $x + y \in \text{interior}(s)$, and any scalar $t \in \mathbb{K}$ with $0 < t \leq 1$, the point $x + t y$ lies in the interior of $s$.
Convex.interior theorem
[ZeroLEOneClass 𝕜] {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (interior s)
Full source 
/-- In a topological vector space, the interior of a convex set is convex. -/
protected theorem Convex.interior [ZeroLEOneClass 𝕜] {s : Set E} (hs : Convex 𝕜 s) :
    Convex 𝕜 (interior s) :=
  convex_iff_openSegment_subset.mpr fun _ hx _ hy =>
    hs.openSegment_closure_interior_subset_interior (interior_subset_closure hx) hy
Convexity of the Interior of a Convex Set in a Topological Vector Space
Informal description
Let $E$ be a topological vector space over an ordered scalar field $\mathbb{K}$ with $0 \leq 1$, and let $s \subseteq E$ be a convex set. Then the interior of $s$ is also convex.
Convex.closure theorem
{s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (closure s)
Full source 
/-- In a topological vector space, the closure of a convex set is convex. -/
protected theorem Convex.closure {s : Set E} (hs : Convex 𝕜 s) : Convex 𝕜 (closure s) :=
  fun x hx y hy a b ha hb hab =>
  let f : E → E → E := fun x' y' => a • x' + b • y'
  have hf : Continuous (Function.uncurry f) :=
    (continuous_fst.const_smul _).add (continuous_snd.const_smul _)
  show f x y ∈ closure s from map_mem_closure₂ hf hx hy fun _ hx' _ hy' => hs hx' hy' ha hb hab
Convexity of the Closure of a Convex Set in a Topological Vector Space
Informal description
Let $E$ be a topological vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. Then the closure $\overline{s}$ is also convex.
Convex.strictConvex' theorem
{s : Set E} (hs : Convex 𝕜 s) (h : (s \ interior s).Pairwise fun x y => ∃ c : 𝕜, lineMap x y c ∈ interior s) : StrictConvex 𝕜 s
Full source 
/-- 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`. -/
protected theorem Convex.strictConvex' {s : Set E} (hs : Convex 𝕜 s)
    (h : (s \ interior s).Pairwise fun x y => ∃ c : 𝕜, lineMap x y c ∈ interior s) :
    StrictConvex 𝕜 s := by
  refine strictConvex_iff_openSegment_subset.2 ?_
  intro x hx y hy hne
  by_cases hx' : x ∈ interior s
  · exact hs.openSegment_interior_self_subset_interior hx' hy
  by_cases hy' : y ∈ interior s
  · exact hs.openSegment_self_interior_subset_interior hx hy'
  rcases h ⟨hx, hx'⟩ ⟨hy, hy'⟩ hne with ⟨c, hc⟩
  refine (openSegment_subset_union x y ⟨c, rfl⟩).trans
    (insert_subset_iff.2 ⟨hc, union_subset ?_ ?_⟩)
  exacts [hs.openSegment_self_interior_subset_interior hx hc,
    hs.openSegment_interior_self_subset_interior hc hy]
Strict Convexity Criterion via Interior Points of Boundary Segments
Informal description
Let $E$ be a topological vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If for any two distinct points $x, y \in s \setminus \text{interior}(s)$, there exists a scalar $c \in \mathbb{K}$ such that the point $(1-c)x + c y$ lies in the interior of $s$, then $s$ is strictly convex.
Convex.strictConvex theorem
{s : Set E} (hs : Convex 𝕜 s) (h : (s \ interior s).Pairwise fun x y => ([x -[𝕜] y] \ frontier s).Nonempty) : StrictConvex 𝕜 s
Full source 
/-- 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`. -/
protected theorem Convex.strictConvex {s : Set E} (hs : Convex 𝕜 s)
    (h : (s \ interior s).Pairwise fun x y => ([x -[𝕜] y][x -[𝕜] y] \ frontier s).Nonempty) :
    StrictConvex 𝕜 s := by
  refine hs.strictConvex' <| h.imp_on fun x hx y hy _ => ?_
  simp only [segment_eq_image_lineMap, ← self_diff_frontier]
  rintro ⟨_, ⟨⟨c, hc, rfl⟩, hcs⟩⟩
  refine ⟨c, hs.segment_subset hx.1 hy.1 ?_, hcs⟩
  exact (segment_eq_image_lineMap 𝕜 x y).symm ▸ mem_image_of_mem _ hc
Strict Convexity Criterion via Non-Frontier Points on Boundary Segments
Informal description
Let $E$ be a topological vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set. If for any two distinct points $x, y \in s \setminus \text{interior}(s)$, the open segment $(x, y)$ contains a point not in the frontier of $s$, then $s$ is strictly convex.
Convex.closure_interior_eq_closure_of_nonempty_interior theorem
{s : Set E} (hs : Convex 𝕜 s) (hs' : (interior s).Nonempty) : closure (interior s) = closure s
Full source 
theorem Convex.closure_interior_eq_closure_of_nonempty_interior {s : Set E} (hs : Convex 𝕜 s)
    (hs' : (interior s).Nonempty) : closure (interior s) = closure s :=
  subset_antisymm (closure_mono interior_subset)
    fun _ h ↦ closure_mono (hs.openSegment_interior_closure_subset_interior hs'.choose_spec h)
      (segment_subset_closure_openSegment (right_mem_segment ..))
Closure of Interior Equals Closure for Convex Sets with Nonempty Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set with nonempty interior. Then the closure of the interior of $s$ is equal to the closure of $s$, i.e., $\overline{\text{interior}(s)} = \overline{s}$.
Convex.interior_closure_eq_interior_of_nonempty_interior theorem
{s : Set E} (hs : Convex 𝕜 s) (hs' : (interior s).Nonempty) : interior (closure s) = interior s
Full source 
theorem Convex.interior_closure_eq_interior_of_nonempty_interior {s : Set E} (hs : Convex 𝕜 s)
    (hs' : (interior s).Nonempty) : interior (closure s) = interior s := by
  refine subset_antisymm ?_ (interior_mono subset_closure)
  intro y hy
  rcases hs' with ⟨x, hx⟩
  have h := AffineMap.lineMap_apply_one (k := 𝕜) x y
  obtain ⟨t, ht1, ht⟩ := AffineMap.lineMap_continuous.tendsto' _ _ h |>.eventually_mem
    (mem_interior_iff_mem_nhds.1 hy) |>.exists_gt
  apply hs.openSegment_interior_closure_subset_interior hx ht
  nth_rw 1 [← AffineMap.lineMap_apply_zero (k := 𝕜) x y, ← image_openSegment]
  exact ⟨1, Ioo_subset_openSegment ⟨zero_lt_one, ht1⟩, h⟩
Interior of Closure Equals Interior for Convex Sets with Nonempty Interior
Informal description
Let $E$ be a vector space over an ordered scalar field $\mathbb{K}$, and let $s \subseteq E$ be a convex set with nonempty interior. Then the interior of the closure of $s$ equals the interior of $s$, i.e., $\text{interior}(\overline{s}) = \text{interior}(s)$.
convex_closed_sInter theorem
{S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s) : Convex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S)
Full source 
theorem convex_closed_sInter {S : Set (Set E)} (h : ∀ s ∈ S, Convex 𝕜 s ∧ IsClosed s) :
    ConvexConvex 𝕜 (⋂₀ S) ∧ IsClosed (⋂₀ S) :=
  ⟨fun _ hx => starConvex_sInter fun _ hs => (h _ hs).1 <| hx _ hs,
    isClosed_sInter fun _ hs => (h _ hs).2⟩
Intersection of Convex Closed Sets is Convex and Closed
Informal description
For any family of sets $S$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, if every set $s \in S$ is convex and closed, then the intersection $\bigcap_{s \in S} s$ is both convex and closed.
closedConvexHull definition
: ClosureOperator (Set E)
Full source 
/-- The convex closed hull of a set `s` is the minimal convex closed set that includes `s`. -/
@[simps! isClosed]
def closedConvexHull : ClosureOperator (Set E) := .ofCompletePred (fun s => ConvexConvex 𝕜 s ∧ IsClosed s)
  fun _ ↦ convex_closed_sInter
Closed convex hull of a set
Informal description
The closed convex hull of a set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$ is the smallest convex and closed set containing $s$. It is defined as the intersection of all convex closed sets that contain $s$.
convex_closedConvexHull theorem
{s : Set E} : Convex 𝕜 (closedConvexHull 𝕜 s)
Full source 
theorem convex_closedConvexHull {s : Set E} :
    Convex 𝕜 (closedConvexHull 𝕜 s) := ((closedConvexHull 𝕜).isClosed_closure s).1
Convexity of the Closed Convex Hull
Informal description
For any set $s$ in a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closed convex hull of $s$ is a convex set.
subset_closedConvexHull theorem
{s : Set E} : s ⊆ closedConvexHull 𝕜 s
Full source 
theorem subset_closedConvexHull {s : Set E} : s ⊆ closedConvexHull 𝕜 s :=
  (closedConvexHull 𝕜).le_closure s
Inclusion of Set in its Closed Convex Hull
Informal description
For any subset $s$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the set $s$ is contained in its closed convex hull, i.e., $s \subseteq \text{closedConvexHull}_{\mathbb{K}}(s)$.
closure_subset_closedConvexHull theorem
{s : Set E} : closure s ⊆ closedConvexHull 𝕜 s
Full source 
theorem closure_subset_closedConvexHull {s : Set E} : closureclosure s ⊆ closedConvexHull 𝕜 s :=
  closure_minimal subset_closedConvexHull isClosed_closedConvexHull
Closure is Contained in Closed Convex Hull
Informal description
For any subset $s$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closure of $s$ is contained in the closed convex hull of $s$, i.e., $\overline{s} \subseteq \text{closedConvexHull}_{\mathbb{K}}(s)$.
closedConvexHull_min theorem
{s t : Set E} (hst : s ⊆ t) (h_conv : Convex 𝕜 t) (h_closed : IsClosed t) : closedConvexHull 𝕜 s ⊆ t
Full source 
theorem closedConvexHull_min {s t : Set E} (hst : s ⊆ t) (h_conv : Convex 𝕜 t)
    (h_closed : IsClosed t) : closedConvexHullclosedConvexHull 𝕜 s ⊆ t :=
  (closedConvexHull 𝕜).closure_min hst ⟨h_conv, h_closed⟩
Minimality Property of Closed Convex Hull: $\text{closedConvexHull}(s) \subseteq t$ for $s \subseteq t$ with $t$ convex and closed
Informal description
Let $s$ and $t$ be subsets of a vector space $E$ over an ordered scalar field $\mathbb{K}$. If $s \subseteq t$, $t$ is convex, and $t$ is closed, then the closed convex hull of $s$ is contained in $t$.
convexHull_subset_closedConvexHull theorem
{s : Set E} : (convexHull 𝕜) s ⊆ (closedConvexHull 𝕜) s
Full source 
theorem convexHull_subset_closedConvexHull {s : Set E} :
    (convexHull 𝕜) s ⊆ (closedConvexHull 𝕜) s :=
  convexHull_min subset_closedConvexHull convex_closedConvexHull
Convex Hull is Subset of Closed Convex Hull
Informal description
For any subset $s$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the convex hull of $s$ is contained in the closed convex hull of $s$, i.e., $\text{convexHull}_{\mathbb{K}}(s) \subseteq \text{closedConvexHull}_{\mathbb{K}}(s)$.
closedConvexHull_closure_eq_closedConvexHull theorem
{s : Set E} : closedConvexHull 𝕜 (closure s) = closedConvexHull 𝕜 s
Full source 
@[simp]
theorem closedConvexHull_closure_eq_closedConvexHull {s : Set E} :
    closedConvexHull 𝕜 (closure s) = closedConvexHull 𝕜 s :=
  subset_antisymm (by
    simpa using ((closedConvexHull 𝕜).monotone (closure_subset_closedConvexHull (𝕜 := 𝕜) (E := E))))
    ((closedConvexHull 𝕜).monotone subset_closure)
Closed Convex Hull of Closure Equals Closed Convex Hull
Informal description
For any subset $s$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closed convex hull of the closure of $s$ equals the closed convex hull of $s$, i.e., \[ \text{closedConvexHull}_{\mathbb{K}}(\overline{s}) = \text{closedConvexHull}_{\mathbb{K}}(s). \]
closedConvexHull_eq_closure_convexHull theorem
{s : Set E} : closedConvexHull 𝕜 s = closure (convexHull 𝕜 s)
Full source 
theorem closedConvexHull_eq_closure_convexHull {s : Set E} :
    closedConvexHull 𝕜 s = closure (convexHull 𝕜 s) := subset_antisymm
  (closedConvexHull_min (subset_trans (subset_convexHull 𝕜 s) subset_closure)
    (Convex.closure (convex_convexHull 𝕜 s)) isClosed_closure)
  (closure_minimal convexHull_subset_closedConvexHull isClosed_closedConvexHull)
Closed Convex Hull Equals Closure of Convex Hull
Informal description
For any subset $s$ of a vector space $E$ over an ordered scalar field $\mathbb{K}$, the closed convex hull of $s$ is equal to the closure of its convex hull, i.e., $\text{closedConvexHull}_{\mathbb{K}}(s) = \overline{\text{convexHull}_{\mathbb{K}}(s)}$.
Set.Finite.isCompact_convexHull theorem
{s : Set E} (hs : s.Finite) : IsCompact (convexHull ℝ s)
Full source 
/-- Convex hull of a finite set is compact. -/
theorem Set.Finite.isCompact_convexHull {s : Set E} (hs : s.Finite) :
    IsCompact (convexHull ℝ s) := by
  rw [hs.convexHull_eq_image]
  apply (@isCompact_stdSimplex _ hs.fintype).image
  haveI := hs.fintype
  apply LinearMap.continuous_on_pi
Compactness of the Convex Hull of a Finite Set in a Real Vector Space
Informal description
For any finite subset $s$ of a real vector space $E$, the convex hull of $s$ is compact.
Set.Finite.isClosed_convexHull theorem
[T2Space E] {s : Set E} (hs : s.Finite) : IsClosed (convexHull ℝ s)
Full source 
/-- Convex hull of a finite set is closed. -/
theorem Set.Finite.isClosed_convexHull [T2Space E] {s : Set E} (hs : s.Finite) :
    IsClosed (convexHull ℝ s) :=
  hs.isCompact_convexHull.isClosed
Closedness of Convex Hull for Finite Sets in Hausdorff Vector Spaces
Informal description
For any finite subset $s$ of a real vector space $E$ that is also a Hausdorff space, the convex hull of $s$ is closed.
Convex.closure_subset_image_homothety_interior_of_one_lt theorem
{s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : closure s ⊆ homothety x t '' interior s
Full source 
/-- 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_image_homothety_interior_of_one_lt {s : Set E} (hs : Convex ℝ s)
    {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
    closureclosure s ⊆ homothety x t '' interior s := by
  intro y hy
  have hne : t ≠ 0 := (one_pos.trans ht).ne'
  refine
    ⟨homothety x t⁻¹ y, hs.openSegment_interior_closure_subset_interior hx hy ?_,
      (AffineEquiv.homothetyUnitsMulHom x (Units.mk0 t hne)).apply_symm_apply y⟩
  rw [openSegment_eq_image_lineMap, ← inv_one, ← inv_Ioi₀ (zero_lt_one' ℝ), ← image_inv_eq_inv,
    image_image, homothety_eq_lineMap]
  exact mem_image_of_mem _ ht
Closure of Convex Set is Contained in Homothety Image of Interior for Scaling Factors $t > 1$
Informal description
Let $E$ be a real vector space and $s \subseteq E$ a convex set. For any point $x$ in the interior of $s$ and any real number $t > 1$, the closure of $s$ is contained in the image of the interior of $s$ under the homothety centered at $x$ with scaling factor $t$. That is, $$\overline{s} \subseteq \{ t(y - x) + x \mid y \in \text{int}(s) \}.$$
Convex.closure_subset_interior_image_homothety_of_one_lt theorem
{s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : closure s ⊆ interior (homothety x t '' s)
Full source 
/-- 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.closure_subset_interior_image_homothety_of_one_lt {s : Set E} (hs : Convex ℝ s)
    {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
    closureclosure s ⊆ interior (homothety x t '' s) :=
  (hs.closure_subset_image_homothety_interior_of_one_lt hx t ht).trans <|
    (homothety_isOpenMap x t (one_pos.trans ht).ne').image_interior_subset _
Closure of Convex Set is Contained in Interior of Homothety Image for Scaling Factors $t > 1$
Informal description
Let $E$ be a real vector space and $s \subseteq E$ a convex set. For any point $x$ in the interior of $s$ and any real number $t > 1$, the closure of $s$ is contained in the interior of the image of $s$ under the homothety centered at $x$ with scaling factor $t$. That is, $$\overline{s} \subseteq \text{int}\big(\{ t(y - x) + x \mid y \in s \}\big).$$
Convex.subset_interior_image_homothety_of_one_lt theorem
{s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : s ⊆ interior (homothety x t '' s)
Full source 
/-- 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 {s : Set E} (hs : Convex ℝ s) {x : E}
    (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) : s ⊆ interior (homothety x t '' s) :=
  subset_closure.trans <| hs.closure_subset_interior_image_homothety_of_one_lt hx t ht
Convex Set is Contained in Interior of its Scaled Image for $t > 1$
Informal description
Let $E$ be a real vector space and $s \subseteq E$ a convex set. For any point $x$ in the interior of $s$ and any real number $t > 1$, the set $s$ is contained in the interior of the image of $s$ under the homothety centered at $x$ with scaling factor $t$. That is, $$s \subseteq \text{int}\big(\{ t(y - x) + x \mid y \in s \}\big).$$
JoinedIn.of_segment_subset theorem
{E : Type*} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {x y : E} {s : Set E} (h : [x -[ℝ] y] ⊆ s) : JoinedIn s x y
Full source 
theorem JoinedIn.of_segment_subset {E : Type*} [AddCommGroup E] [Module ℝ E]
    [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E]
    {x y : E} {s : Set E} (h : [x -[ℝ] y][x -[ℝ] y] ⊆ s) : JoinedIn s x y := by
  have A : Continuous (fun t ↦ (1 - t) • x + t • y : ℝ → E) := by fun_prop
  apply JoinedIn.ofLine A.continuousOn (by simp) (by simp)
  convert h
  rw [segment_eq_image ℝ x y]
Path-connectedness of Convex Sets via Segment Inclusion
Informal description
Let $E$ be a topological vector space over $\mathbb{R}$ with continuous addition and scalar multiplication. For any subset $s \subseteq E$ and any two points $x, y \in E$, if the closed segment $[x, y] := \{ (1-t)x + t y \mid t \in [0,1] \}$ is contained in $s$, then $x$ and $y$ are joined by a path within $s$.
Convex.isPathConnected theorem
{s : Set E} (hconv : Convex ℝ s) (hne : s.Nonempty) : IsPathConnected s
Full source 
/-- A nonempty convex set is path connected. -/
protected theorem Convex.isPathConnected {s : Set E} (hconv : Convex ℝ s) (hne : s.Nonempty) :
    IsPathConnected s := by
  refine isPathConnected_iff.mpr ⟨hne, ?_⟩
  intro x x_in y y_in
  exact JoinedIn.of_segment_subset ((segment_subset_iff ℝ).2 (hconv x_in y_in))
Path-Connectedness of Nonempty Convex Sets in Real Topological Vector Spaces
Informal description
Let $E$ be a real topological vector space. For any nonempty convex subset $s \subseteq E$, the set $s$ is path-connected.
Convex.isConnected theorem
{s : Set E} (h : Convex ℝ s) (hne : s.Nonempty) : IsConnected s
Full source 
/-- A nonempty convex set is connected. -/
protected theorem Convex.isConnected {s : Set E} (h : Convex ℝ s) (hne : s.Nonempty) :
    IsConnected s :=
  (h.isPathConnected hne).isConnected
Connectedness of Nonempty Convex Sets in Real Topological Vector Spaces
Informal description
Let $E$ be a real topological vector space. For any nonempty convex subset $s \subseteq E$, the set $s$ is connected.
Convex.isPreconnected theorem
{s : Set E} (h : Convex ℝ s) : IsPreconnected s
Full source 
/-- A convex set is preconnected. -/
protected theorem Convex.isPreconnected {s : Set E} (h : Convex ℝ s) : IsPreconnected s :=
  s.eq_empty_or_nonempty.elim (fun h => h.symm ▸ isPreconnected_empty) fun hne =>
    (h.isConnected hne).isPreconnected
Preconnectedness of Convex Sets in Real Topological Vector Spaces
Informal description
Let $E$ be a real topological vector space. For any convex subset $s \subseteq E$, the set $s$ is preconnected.
IsTopologicalAddGroup.pathConnectedSpace theorem
: PathConnectedSpace E
Full source 
/-- Every topological vector space over ℝ is path connected.

Not an instance, because it creates enormous TC subproblems (turn on `pp.all`).
-/
protected theorem IsTopologicalAddGroup.pathConnectedSpace : PathConnectedSpace E :=
  pathConnectedSpace_iff_univ.mpr <| convex_univ.isPathConnected ⟨(0 : E), trivial⟩
Path-Connectedness of Real Topological Vector Spaces
Informal description
Every real topological vector space $E$ is path-connected as a topological space.
isPathConnected_compl_of_isPathConnected_compl_zero theorem
[ContinuousSMul ℝ E] {p q : Submodule ℝ E} (hpq : IsCompl p q) (hpc : IsPathConnected ({0}ᶜ : Set p)) : IsPathConnected (qᶜ : Set E)
Full source 
/-- 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`. -/
theorem isPathConnected_compl_of_isPathConnected_compl_zero [ContinuousSMul ℝ E]
    {p q : Submodule ℝ E} (hpq : IsCompl p q) (hpc : IsPathConnected ({0}{0}ᶜ : Set p)) :
    IsPathConnected (qᶜ : Set E) := by
  rw [isPathConnected_iff] at hpc ⊢
  constructor
  · rcases hpc.1 with ⟨a, ha⟩
    exact ⟨a, mt (Submodule.eq_zero_of_coe_mem_of_disjoint hpq.disjoint) ha⟩
  · intro x hx y hy
    have : ππ hpq x ≠ 0π hpq x ≠ 0 ∧ π hpq y ≠ 0 := by
      constructor <;> intro h <;> rw [Submodule.linearProjOfIsCompl_apply_eq_zero_iff hpq] at h <;>
        [exact hx h; exact hy h]
    rcases hpc.2 (π hpq x) this.1 (π hpq y) this.2 with ⟨γ₁, hγ₁⟩
    let γ₂ := PathConnectedSpace.somePath (π hpq.symm x) (π hpq.symm y)
    let γ₁' : Path (_ : E) _ := γ₁.map continuous_subtype_val
    let γ₂' : Path (_ : E) _ := γ₂.map continuous_subtype_val
    refine ⟨(γ₁'.add γ₂').cast (Submodule.linear_proj_add_linearProjOfIsCompl_eq_self hpq x).symm
      (Submodule.linear_proj_add_linearProjOfIsCompl_eq_self hpq y).symm, fun t ↦ ?_⟩
    rw [Path.cast_coe, Path.add_apply]
    change γ₁ t + (γ₂ t : E) ∉ q
    rw [← Submodule.linearProjOfIsCompl_apply_eq_zero_iff hpq, LinearMap.map_add,
      Submodule.linearProjOfIsCompl_apply_right, add_zero,
      Submodule.linearProjOfIsCompl_apply_eq_zero_iff]
    exact mt (Submodule.eq_zero_of_coe_mem_of_disjoint hpq.disjoint) (hγ₁ t)
Path-Connectedness of Complement of Complementary Subspace in Topological Vector Space
Informal description
Let $E$ be a real topological vector space with continuous scalar multiplication, and let $p$ and $q$ be complementary subspaces of $E$ (i.e., $p \cap q = \{0\}$ and $p + q = E$). If the complement of $\{0\}$ in $p$ is path-connected, then the complement of $q$ in $E$ is also path-connected.
Convex.nontrivial_iff_nonempty_interior theorem
{s : Set 𝕜} (hs : Convex 𝕜 s) : s.Nontrivial ↔ (interior s).Nonempty
Full source 
theorem Convex.nontrivial_iff_nonempty_interior {s : Set 𝕜} (hs : Convex 𝕜 s) :
    s.Nontrivial ↔ (interior s).Nonempty := by
  constructor
  · rintro ⟨x, hx, y, hy, h⟩
    have hs' := Nonempty.mono <| interior_mono <| hs.segment_subset hx hy
    rw [segment_eq_Icc', interior_Icc, nonempty_Ioo, inf_lt_sup] at hs'
    exact hs' h
  · rintro ⟨x, hx⟩
    rcases eq_singleton_or_nontrivial (interior_subset hx) with rfl | h
    · rw [interior_singleton] at hx
      exact hx.elim
    · exact h
Nontriviality of Convex Set Equivalent to Nonempty Interior
Informal description
For a convex set $s$ in a vector space over an ordered scalar field $\mathbb{K}$, the set $s$ is nontrivial (contains at least two distinct points) if and only if its interior is nonempty.