Mathlib.Analysis.Convex.Segment

segment definition

(x y : E) : Set E

Full source

/-- Segments in a vector space. -/
def segment (x y : E) : Set E :=
  { z : E | ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a • x + b • y = z }

Closed segment in a vector space

Informal description

The closed segment joining two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$ is the set of all points $z$ that can be expressed as $z = a \cdot x + b \cdot y$ for some scalars $a, b \in \mathbb{K}$ with $a, b \geq 0$ and $a + b = 1$.

openSegment definition

(x y : E) : Set E

Full source

/-- Open segment in a vector space. Note that `openSegment 𝕜 x x = {x}` instead of being `∅` when
the base semiring has some element between `0` and `1`.
Denoted as `[x -[𝕜] y]` within the `Convex` namespace. -/
def openSegment (x y : E) : Set E :=
  { z : E | ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a • x + b • y = z }

Open segment in a vector space

Informal description

The open segment between two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$ is the set of all points $z$ that can be expressed as $z = a \cdot x + b \cdot y$ for some scalars $a, b \in \mathbb{K}$ with $a, b > 0$ and $a + b = 1$. Note that when $x = y$, the open segment is $\{x\}$ rather than empty, provided the base semiring has elements between $0$ and $1$.

Convex.term[_-[_]_] definition

: Lean.ParserDescr✝

Full source

@[inherit_doc] scoped[Convex] notation (priority := high) "[" x " -[" 𝕜 "] " y "]" => segment 𝕜 x y

Closed segment notation `[x -[𝕜] y]`

Informal description

The notation `[x -[𝕜] y]` represents the closed segment joining two points `x` and `y` in a 𝕜-vector space, which is defined as the set of all points that can be expressed as `(1 - t) • x + t • y` for some `t ∈ [0, 1]`.

segment_eq_image₂ theorem

 (x y : E) : [x -[𝕜] y] = (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' {p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1}

Full source

theorem segment_eq_image₂ (x y : E) :
    [x -[𝕜] y] =
      (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' { p | 0 ≤ p.1 ∧ 0 ≤ p.2 ∧ p.1 + p.2 = 1 } := by
  simp only [segment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]

Closed Segment as Image of Linear Combination

Informal description

For any points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the closed segment $[x -[𝕜] y]$ is equal to the image of the function $(a, b) \mapsto a \cdot x + b \cdot y$ applied to the set of pairs $(a, b) \in \mathbb{K} \times \mathbb{K}$ such that $a, b \geq 0$ and $a + b = 1$.

openSegment_eq_image₂ theorem

 (x y : E) : openSegment 𝕜 x y = (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' {p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1}

Full source

theorem openSegment_eq_image₂ (x y : E) :
    openSegment 𝕜 x y =
      (fun p : 𝕜 × 𝕜 => p.1 • x + p.2 • y) '' { p | 0 < p.1 ∧ 0 < p.2 ∧ p.1 + p.2 = 1 } := by
  simp only [openSegment, image, Prod.exists, mem_setOf_eq, exists_prop, and_assoc]

Open Segment as Image of Positive Linear Combination

Informal description

For any points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the open segment between $x$ and $y$ is equal to the image of the function $(a, b) \mapsto a \cdot x + b \cdot y$ applied to the set of pairs $(a, b) \in \mathbb{K} \times \mathbb{K}$ such that $a, b > 0$ and $a + b = 1$.

segment_symm theorem

(x y : E) : [x -[𝕜] y] = [y -[𝕜] x]

Full source

theorem segment_symm (x y : E) : [x -[𝕜] y] = [y -[𝕜] x] :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, H⟩ => ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
      fun ⟨a, b, ha, hb, hab, H⟩ =>
      ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩

Symmetry of Closed Segment: $[x -[𝕜] y] = [y -[𝕜] x]$

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the closed segment joining $x$ and $y$ is equal to the closed segment joining $y$ and $x$, i.e., $[x -[𝕜] y] = [y -[𝕜] x]$.

openSegment_symm theorem

(x y : E) : openSegment 𝕜 x y = openSegment 𝕜 y x

Full source

theorem openSegment_symm (x y : E) : openSegment 𝕜 x y = openSegment 𝕜 y x :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, H⟩ => ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩,
      fun ⟨a, b, ha, hb, hab, H⟩ =>
      ⟨b, a, hb, ha, (add_comm _ _).trans hab, (add_comm _ _).trans H⟩⟩

Symmetry of Open Segment: $\text{openSegment}_{\mathbb{K}}(x, y) = \text{openSegment}_{\mathbb{K}}(y, x)$

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the open segment joining $x$ and $y$ is equal to the open segment joining $y$ and $x$, i.e., $\text{openSegment}_{\mathbb{K}}(x, y) = \text{openSegment}_{\mathbb{K}}(y, x)$.

openSegment_subset_segment theorem

(x y : E) : openSegment 𝕜 x y ⊆ [x -[𝕜] y]

Full source

theorem openSegment_subset_segment (x y : E) : openSegmentopenSegment 𝕜 x y ⊆ [x -[𝕜] y] :=
  fun _ ⟨a, b, ha, hb, hab, hz⟩ => ⟨a, b, ha.le, hb.le, hab, hz⟩

Open Segment is Subset of Closed Segment

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the open segment joining $x$ and $y$ is a subset of the closed segment joining $x$ and $y$, i.e., $\text{openSegment}_{\mathbb{K}}(x, y) \subseteq [x -[𝕜] y]$.

segment_subset_iff theorem

: [x -[𝕜] y] ⊆ s ↔ ∀ a b : 𝕜, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem segment_subset_iff :
    [x -[𝕜] y][x -[𝕜] y] ⊆ s[x -[𝕜] y] ⊆ s ↔ ∀ a b : 𝕜, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s :=
  ⟨fun H a b ha hb hab => H ⟨a, b, ha, hb, hab, rfl⟩, fun H _ ⟨a, b, ha, hb, hab, hz⟩ =>
    hz ▸ H a b ha hb hab⟩

Characterization of Closed Segment Containment: $[x -[\mathbb{K}] y] \subseteq s \leftrightarrow \forall a, b \geq 0, a + b = 1 \Rightarrow a x + b y \in s$

Informal description

For a closed segment $[x -[\mathbb{K}] y]$ in a $\mathbb{K}$-vector space and a set $s$, the segment is contained in $s$ if and only if for all non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the point $a \cdot x + b \cdot y$ belongs to $s$.

openSegment_subset_iff theorem

: openSegment 𝕜 x y ⊆ s ↔ ∀ a b : 𝕜, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem openSegment_subset_iff :
    openSegmentopenSegment 𝕜 x y ⊆ sopenSegment 𝕜 x y ⊆ s ↔ ∀ a b : 𝕜, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s :=
  ⟨fun H a b ha hb hab => H ⟨a, b, ha, hb, hab, rfl⟩, fun H _ ⟨a, b, ha, hb, hab, hz⟩ =>
    hz ▸ H a b ha hb hab⟩

Characterization of Open Segment Containment via Convex Combinations

Informal description

For any subset $s$ of a $\mathbb{K}$-vector space $E$, the open segment between two points $x$ and $y$ is contained in $s$ if and only if for all positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ belongs to $s$.

left_mem_segment theorem

(x y : E) : x ∈ [x -[𝕜] y]

Full source

theorem left_mem_segment (x y : E) : x ∈ [x -[𝕜] y] :=
  ⟨1, 0, zero_le_one, le_refl 0, add_zero 1, by rw [zero_smul, one_smul, add_zero]⟩

Left Endpoint Belongs to Closed Segment

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the point $x$ belongs to the closed segment joining $x$ and $y$, denoted $[x -[\mathbb{K}] y]$.

right_mem_segment theorem

(x y : E) : y ∈ [x -[𝕜] y]

Full source

theorem right_mem_segment (x y : E) : y ∈ [x -[𝕜] y] :=
  segment_symm 𝕜 y x ▸ left_mem_segment 𝕜 y x

Right Endpoint Belongs to Closed Segment

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the point $y$ belongs to the closed segment joining $x$ and $y$, denoted $[x -[\mathbb{K}] y]$.

segment_same theorem

(x : E) : [x -[𝕜] x] = { x }

Full source

@[simp]
theorem segment_same (x : E) : [x -[𝕜] x] = {x} :=
  Set.ext fun z =>
    ⟨fun ⟨a, b, _, _, hab, hz⟩ => by
      simpa only [(add_smul _ _ _).symm, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
      fun h => mem_singleton_iff.1 h ▸ left_mem_segment 𝕜 z z⟩

Closed Segment at a Point is Singleton: $[x -[\mathbb{K}] x] = \{x\}$

Informal description

For any point $x$ in a $\mathbb{K}$-vector space $E$, the closed segment joining $x$ to itself is equal to the singleton set $\{x\}$, i.e., $[x -[\mathbb{K}] x] = \{x\}$.

insert_endpoints_openSegment theorem

(x y : E) : insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y]

Full source

theorem insert_endpoints_openSegment (x y : E) :
    insert x (insert y (openSegment 𝕜 x y)) = [x -[𝕜] y] := by
  simp only [subset_antisymm_iff, insert_subset_iff, left_mem_segment, right_mem_segment,
    openSegment_subset_segment, true_and]
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  refine hb.eq_or_gt.imp ?_ fun hb' => ha.eq_or_gt.imp ?_ fun ha' => ?_
  · rintro rfl
    rw [← add_zero a, hab, one_smul, zero_smul, add_zero]
  · rintro rfl
    rw [← zero_add b, hab, one_smul, zero_smul, zero_add]
  · exact ⟨a, b, ha', hb', hab, rfl⟩

Closed Segment as Open Segment with Endpoints: $[x -[\mathbb{K}] y] = \{x,y\} \cup \text{openSegment}_{\mathbb{K}}(x,y)$

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the set obtained by inserting the endpoints $x$ and $y$ into the open segment between $x$ and $y$ equals the closed segment joining $x$ and $y$. In other words: \[ \{x\} \cup \{y\} \cup \text{openSegment}_{\mathbb{K}}(x,y) = [x -[\mathbb{K}] y] \]

mem_openSegment_of_ne_left_right theorem

(hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x -[𝕜] y]) : z ∈ openSegment 𝕜 x y

Full source

theorem mem_openSegment_of_ne_left_right (hx : x ≠ z) (hy : y ≠ z) (hz : z ∈ [x -[𝕜] y]) :
    z ∈ openSegment 𝕜 x y := by
  rw [← insert_endpoints_openSegment] at hz
  exact (hz.resolve_left hx.symm).resolve_left hy.symm

Non-Endpoint in Closed Segment Implies Membership in Open Segment

Informal description

For any points $x$, $y$, and $z$ in a $\mathbb{K}$-vector space $E$, if $x \neq z$, $y \neq z$, and $z$ belongs to the closed segment $[x -[\mathbb{K}] y]$, then $z$ belongs to the open segment between $x$ and $y$.

openSegment_subset_iff_segment_subset theorem

(hx : x ∈ s) (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s

Full source

theorem openSegment_subset_iff_segment_subset (hx : x ∈ s) (hy : y ∈ s) :
    openSegmentopenSegment 𝕜 x y ⊆ sopenSegment 𝕜 x y ⊆ s ↔ [x -[𝕜] y] ⊆ s := by
  simp only [← insert_endpoints_openSegment, insert_subset_iff, *, true_and]

Open Segment Subset Equivalence to Closed Segment Subset

Informal description

For any two points $x$ and $y$ in a set $s$ in a $\mathbb{K}$-vector space $E$, the open segment between $x$ and $y$ is a subset of $s$ if and only if the closed segment between $x$ and $y$ is a subset of $s$. In other words: \[ \text{openSegment}_{\mathbb{K}}(x,y) \subseteq s \leftrightarrow [x -[𝕜] y] \subseteq s \]

openSegment_same theorem

(x : E) : openSegment 𝕜 x x = { x }

Full source

@[simp]
theorem openSegment_same (x : E) : openSegment 𝕜 x x = {x} :=
  Set.ext fun z =>
    ⟨fun ⟨a, b, _, _, hab, hz⟩ => by
      simpa only [← add_smul, mem_singleton_iff, hab, one_smul, eq_comm] using hz,
    fun h : z = x => by
      obtain ⟨a, ha₀, ha₁⟩ := DenselyOrdered.dense (0 : 𝕜) 1 zero_lt_one
      refine ⟨a, 1 - a, ha₀, sub_pos_of_lt ha₁, add_sub_cancel _ _, ?_⟩
      rw [← add_smul, add_sub_cancel, one_smul, h]⟩

Open Segment at a Point is Singleton

Informal description

For any point $x$ in a vector space $E$ over a field $\mathbb{K}$, the open segment between $x$ and itself is the singleton set $\{x\}$.

segment_eq_image theorem

(x y : E) : [x -[𝕜] y] = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Icc (0 : 𝕜) 1

Full source

theorem segment_eq_image (x y : E) :
    [x -[𝕜] y] = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Icc (0 : 𝕜) 1 :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
      ⟨b, ⟨hb, hab ▸ le_add_of_nonneg_left ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
      fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_nonneg.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩

Closed Segment as Affine Image of Unit Interval

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the closed segment $[x -[𝕜] y]$ is equal to the image of the closed unit interval $[0,1] \subseteq \mathbb{K}$ under the affine map $\theta \mapsto (1-\theta)x + \theta y$. In other words: \[ [x -[𝕜] y] = \{(1-\theta)x + \theta y \mid \theta \in [0,1]\} \]

openSegment_eq_image theorem

(x y : E) : openSegment 𝕜 x y = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Ioo (0 : 𝕜) 1

Full source

theorem openSegment_eq_image (x y : E) :
    openSegment 𝕜 x y = (fun θ : 𝕜 => (1 - θ) • x + θ • y) '' Ioo (0 : 𝕜) 1 :=
  Set.ext fun _ =>
    ⟨fun ⟨a, b, ha, hb, hab, hz⟩ =>
      ⟨b, ⟨hb, hab ▸ lt_add_of_pos_left _ ha⟩, hab ▸ hz ▸ by simp only [add_sub_cancel_right]⟩,
      fun ⟨θ, ⟨hθ₀, hθ₁⟩, hz⟩ => ⟨1 - θ, θ, sub_pos.2 hθ₁, hθ₀, sub_add_cancel _ _, hz⟩⟩

Open Segment as Affine Image of Unit Interval

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the open segment between $x$ and $y$ is equal to the image of the open unit interval $(0,1) \subseteq \mathbb{K}$ under the affine map $\theta \mapsto (1-\theta)x + \theta y$. In other words: \[ \text{openSegment}_{\mathbb{K}}(x,y) = \{(1-\theta)x + \theta y \mid \theta \in (0,1)\} \]

segment_eq_image' theorem

(x y : E) : [x -[𝕜] y] = (fun θ : 𝕜 => x + θ • (y - x)) '' Icc (0 : 𝕜) 1

Full source

theorem segment_eq_image' (x y : E) :
    [x -[𝕜] y] = (fun θ : 𝕜 => x + θ • (y - x)) '' Icc (0 : 𝕜) 1 := by
  convert segment_eq_image 𝕜 x y using 2
  simp only [smul_sub, sub_smul, one_smul]
  abel

Closed Segment as Affine Image of Unit Interval via Relative Coordinates

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the closed segment $[x -[𝕜] y]$ is equal to the image of the closed unit interval $[0,1] \subseteq \mathbb{K}$ under the affine map $\theta \mapsto x + \theta(y - x)$. In other words: \[ [x -[𝕜] y] = \{x + \theta(y - x) \mid \theta \in [0,1]\} \]

openSegment_eq_image' theorem

(x y : E) : openSegment 𝕜 x y = (fun θ : 𝕜 => x + θ • (y - x)) '' Ioo (0 : 𝕜) 1

Full source

theorem openSegment_eq_image' (x y : E) :
    openSegment 𝕜 x y = (fun θ : 𝕜 => x + θ • (y - x)) '' Ioo (0 : 𝕜) 1 := by
  convert openSegment_eq_image 𝕜 x y using 2
  simp only [smul_sub, sub_smul, one_smul]
  abel

Open Segment as Affine Image of Unit Interval via Difference Vector

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the open segment between $x$ and $y$ is equal to the image of the open unit interval $(0,1) \subseteq \mathbb{K}$ under the affine map $\theta \mapsto x + \theta(y - x)$. In other words: \[ \text{openSegment}_{\mathbb{K}}(x,y) = \{x + \theta(y - x) \mid \theta \in (0,1)\} \]

segment_eq_image_lineMap theorem

(x y : E) : [x -[𝕜] y] = AffineMap.lineMap x y '' Icc (0 : 𝕜) 1

Full source

theorem segment_eq_image_lineMap (x y : E) : [x -[𝕜] y] =
    AffineMap.lineMapAffineMap.lineMap x y '' Icc (0 : 𝕜) 1 := by
  convert segment_eq_image 𝕜 x y using 2
  exact AffineMap.lineMap_apply_module _ _ _

Closed Segment as Affine Image of Unit Interval via Line Map

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the closed segment $[x -[𝕜] y]$ is equal to the image of the closed unit interval $[0,1] \subseteq \mathbb{K}$ under the affine map $\text{AffineMap.lineMap}\,x\,y$, which maps $\theta \in \mathbb{K}$ to $(1-\theta)x + \theta y$. In other words: \[ [x -[𝕜] y] = \{(1-\theta)x + \theta y \mid \theta \in [0,1]\} \]

openSegment_eq_image_lineMap theorem

(x y : E) : openSegment 𝕜 x y = AffineMap.lineMap x y '' Ioo (0 : 𝕜) 1

Full source

theorem openSegment_eq_image_lineMap (x y : E) :
    openSegment 𝕜 x y = AffineMap.lineMapAffineMap.lineMap x y '' Ioo (0 : 𝕜) 1 := by
  convert openSegment_eq_image 𝕜 x y using 2
  exact AffineMap.lineMap_apply_module _ _ _

Open Segment as Affine Image of Unit Interval via Line Map

Informal description

For any two points $x$ and $y$ in a vector space $E$ over a field $\mathbb{K}$, the open segment between $x$ and $y$ is equal to the image of the open unit interval $(0,1) \subseteq \mathbb{K}$ under the affine map $\text{lineMap}(x,y) : \mathbb{K} \to E$ defined by $\theta \mapsto (1-\theta)x + \theta y$. In other words: \[ \text{openSegment}_{\mathbb{K}}(x,y) = \{\text{lineMap}(x,y)(\theta) \mid \theta \in (0,1)\} \]

image_segment theorem

(f : E →ᵃ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b]

Full source

@[simp]
theorem image_segment (f : E →ᵃ[𝕜] F) (a b : E) : f '' [a -[𝕜] b] = [f a -[𝕜] f b] :=
  Set.ext fun x => by
    simp_rw [segment_eq_image_lineMap, mem_image, exists_exists_and_eq_and, AffineMap.apply_lineMap]

Image of Closed Segment under Affine Map is Closed Segment of Images

Informal description

For any affine map $f \colon E \to F$ between vector spaces over a field $\mathbb{K}$, and any two points $a, b \in E$, the image of the closed segment $[a -[𝕜] b]$ under $f$ is equal to the closed segment $[f(a) -[𝕜] f(b)]$ in $F$. In other words: \[ f([a, b]) = [f(a), f(b)] \] where $[a, b]$ denotes the closed segment joining $a$ and $b$ in $E$, and $[f(a), f(b)]$ denotes the closed segment joining $f(a)$ and $f(b)$ in $F$.

image_openSegment theorem

(f : E →ᵃ[𝕜] F) (a b : E) : f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b)

Full source

@[simp]
theorem image_openSegment (f : E →ᵃ[𝕜] F) (a b : E) :
    f '' openSegment 𝕜 a b = openSegment 𝕜 (f a) (f b) :=
  Set.ext fun x => by
    simp_rw [openSegment_eq_image_lineMap, mem_image, exists_exists_and_eq_and,
      AffineMap.apply_lineMap]

Affine Image of Open Segment Equals Open Segment of Images

Informal description

Let $E$ and $F$ be vector spaces over a field $\mathbb{K}$, and let $f : E \to F$ be an affine map. For any two points $a, b \in E$, the image of the open segment $\text{openSegment}_{\mathbb{K}}(a,b)$ under $f$ equals the open segment between $f(a)$ and $f(b)$ in $F$, i.e., \[ f(\text{openSegment}_{\mathbb{K}}(a,b)) = \text{openSegment}_{\mathbb{K}}(f(a), f(b)). \]

vadd_segment theorem

[AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) : a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c]

Full source

@[simp]
theorem vadd_segment [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) :
    a +ᵥ [b -[𝕜] c] = [a +ᵥ b -[𝕜] a +ᵥ c] :=
  image_segment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

Translation of Closed Segment Equals Closed Segment of Translations

Informal description

Let $G$ be an additive torsor acting on a $\mathbb{K}$-vector space $E$ with a compatible vector addition structure. For any element $a \in G$ and any points $b, c \in E$, the translation of the closed segment $[b, c]$ by $a$ is equal to the closed segment formed by translating $b$ and $c$ by $a$, i.e., \[ a + [b, c] = [a + b, a + c]. \]

vadd_openSegment theorem

 [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) : a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c)

Full source

@[simp]
theorem vadd_openSegment [AddTorsor G E] [VAddCommClass G E E] (a : G) (b c : E) :
    a +ᵥ openSegment 𝕜 b c = openSegment 𝕜 (a +ᵥ b) (a +ᵥ c) :=
  image_openSegment 𝕜 ⟨_, LinearMap.id, fun _ _ => vadd_comm _ _ _⟩ b c

Translation Invariance of Open Segment under Torsor Action

Informal description

Let $G$ be an additive torsor acting on a $\mathbb{K}$-vector space $E$, with the action satisfying the commutative property `VAddCommClass`. For any element $a \in G$ and any points $b, c \in E$, the translation of the open segment $\text{openSegment}_{\mathbb{K}}(b, c)$ by $a$ equals the open segment between the translated points $a +ᵥ b$ and $a +ᵥ c$, i.e., \[ a +ᵥ \text{openSegment}_{\mathbb{K}}(b, c) = \text{openSegment}_{\mathbb{K}}(a +ᵥ b, a +ᵥ c). \]

mem_segment_translate theorem

(a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c]

Full source

@[simp]
theorem mem_segment_translate (a : E) {x b c} : a + x ∈ [a + b -[𝕜] a + c]a + x ∈ [a + b -[𝕜] a + c] ↔ x ∈ [b -[𝕜] c] := by
  simp_rw [← vadd_eq_add, ← vadd_segment, vadd_mem_vadd_set_iff]

Translation Invariance of Closed Segment Membership

Informal description

For any point $a$ in a $\mathbb{K}$-vector space $E$, and for any points $x, b, c \in E$, the translated point $a + x$ belongs to the closed segment $[a + b, a + c]$ if and only if $x$ belongs to the closed segment $[b, c]$.

mem_openSegment_translate theorem

(a : E) {x b c : E} : a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c

Full source

@[simp]
theorem mem_openSegment_translate (a : E) {x b c : E} :
    a + x ∈ openSegment 𝕜 (a + b) (a + c)a + x ∈ openSegment 𝕜 (a + b) (a + c) ↔ x ∈ openSegment 𝕜 b c := by
  simp_rw [← vadd_eq_add, ← vadd_openSegment, vadd_mem_vadd_set_iff]

Translation Invariance of Open Segment Membership

Informal description

For any point $a$ in a $\mathbb{K}$-vector space $E$, and for any points $x, b, c \in E$, the translated point $a + x$ belongs to the open segment between $a + b$ and $a + c$ if and only if $x$ belongs to the open segment between $b$ and $c$.

segment_translate_preimage theorem

(a b c : E) : (fun x => a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c]

Full source

theorem segment_translate_preimage (a b c : E) :
    (fun x => a + x) ⁻¹' [a + b -[𝕜] a + c] = [b -[𝕜] c] :=
  Set.ext fun _ => mem_segment_translate 𝕜 a

Preimage of Translated Closed Segment Equals Original Closed Segment

Informal description

For any points $a, b, c$ in a $\mathbb{K}$-vector space $E$, the preimage of the closed segment $[a + b, a + c]$ under the translation map $x \mapsto a + x$ is equal to the closed segment $[b, c]$. In other words, $$(x \mapsto a + x)^{-1}\big([a + b, a + c]\big) = [b, c].$$

openSegment_translate_preimage theorem

(a b c : E) : (fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c

Full source

theorem openSegment_translate_preimage (a b c : E) :
    (fun x => a + x) ⁻¹' openSegment 𝕜 (a + b) (a + c) = openSegment 𝕜 b c :=
  Set.ext fun _ => mem_openSegment_translate 𝕜 a

Preimage of Translated Open Segment Equals Original Open Segment

Informal description

For any points $a, b, c$ in a $\mathbb{K}$-vector space $E$, the preimage of the open segment between $a + b$ and $a + c$ under the translation map $x \mapsto a + x$ is equal to the open segment between $b$ and $c$. In other words, $$(x \mapsto a + x)^{-1}\big(\text{openSegment}_{\mathbb{K}}(a + b, a + c)\big) = \text{openSegment}_{\mathbb{K}}(b, c).$$

segment_translate_image theorem

(a b c : E) : (fun x => a + x) '' [b -[𝕜] c] = [a + b -[𝕜] a + c]

Full source

theorem segment_translate_image (a b c : E) : (fun x => a + x) '' [b -[𝕜] c] = [a + b -[𝕜] a + c] :=
  segment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ <| add_left_surjective a

Image of Closed Segment under Translation Equals Translated Closed Segment

Informal description

For any points $a, b, c$ in a $\mathbb{K}$-vector space $E$, the image of the closed segment $[b, c]$ under the translation map $x \mapsto a + x$ is equal to the closed segment $[a + b, a + c]$. In other words, $$(x \mapsto a + x)\big([b, c]\big) = [a + b, a + c].$$

openSegment_translate_image theorem

(a b c : E) : (fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c)

Full source

theorem openSegment_translate_image (a b c : E) :
    (fun x => a + x) '' openSegment 𝕜 b c = openSegment 𝕜 (a + b) (a + c) :=
  openSegment_translate_preimage 𝕜 a b c ▸ image_preimage_eq _ <| add_left_surjective a

Image of Open Segment under Translation is Open Segment

Informal description

For any points $a, b, c$ in a $\mathbb{K}$-vector space $E$, the image of the open segment between $b$ and $c$ under the translation map $x \mapsto a + x$ is equal to the open segment between $a + b$ and $a + c$. In other words, $$(x \mapsto a + x)\big(\text{openSegment}_{\mathbb{K}}(b, c)\big) = \text{openSegment}_{\mathbb{K}}(a + b, a + c).$$

segment_inter_subset_endpoint_of_linearIndependent_sub theorem

{c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) : [c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ { c }

Full source

lemma segment_inter_subset_endpoint_of_linearIndependent_sub
    {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) :
    [c -[𝕜] x][c -[𝕜] x] ∩ [c -[𝕜] y][c -[𝕜] x] ∩ [c -[𝕜] y] ⊆ {c} := by
  intro z ⟨hzt, hzs⟩
  rw [segment_eq_image, mem_image] at hzt hzs
  rcases hzt with ⟨p, ⟨p0, p1⟩, rfl⟩
  rcases hzs with ⟨q, ⟨q0, q1⟩, H⟩
  have Hx : x = (x - c) + c := by abel
  have Hy : y = (y - c) + c := by abel
  rw [Hx, Hy, smul_add, smul_add] at H
  have : c + q • (y - c) = c + p • (x - c) := by
    convert H using 1 <;> simp [sub_smul]
  obtain ⟨rfl, rfl⟩ : p = 0 ∧ q = 0 := h.eq_zero_of_pair' ((add_right_inj c).1 this).symm
  simp

Intersection of Segments with Common Endpoint is Trivial under Linear Independence

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$, and let $c, x, y \in E$. If the vectors $x - c$ and $y - c$ are linearly independent in $E$, then the intersection of the closed segments $[c, x]$ and $[c, y]$ is contained in the singleton set $\{c\}$.

segment_inter_eq_endpoint_of_linearIndependent_sub theorem

 [ZeroLEOneClass 𝕜] {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) : [c -[𝕜] x] ∩ [c -[𝕜] y] = { c }

Full source

lemma segment_inter_eq_endpoint_of_linearIndependent_sub [ZeroLEOneClass 𝕜]
    {c x y : E} (h : LinearIndependent 𝕜 ![x - c, y - c]) :
    [c -[𝕜] x][c -[𝕜] x] ∩ [c -[𝕜] y] = {c} := by
  refine (segment_inter_subset_endpoint_of_linearIndependent_sub 𝕜 h).antisymm ?_
  simp [singleton_subset_iff, left_mem_segment]

Intersection of Segments with Common Endpoint is Exactly the Endpoint under Linear Independence

Informal description

Let $E$ be a vector space over a field $\mathbb{K}$ with $0 \leq 1$ in $\mathbb{K}$, and let $c, x, y \in E$. If the vectors $x - c$ and $y - c$ are linearly independent in $E$, then the intersection of the closed segments $[c, x]$ and $[c, y]$ is equal to the singleton set $\{c\}$.

sameRay_of_mem_segment theorem

 [CommRing 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y z : E} (h : x ∈ [y -[𝕜] z]) :
  SameRay 𝕜 (x - y) (z - x)

Full source

theorem sameRay_of_mem_segment [CommRing 𝕜] [PartialOrder 𝕜] [IsStrictOrderedRing 𝕜]
    [AddCommGroup E] [Module 𝕜 E] {x y z : E}
    (h : x ∈ [y -[𝕜] z]) : SameRay 𝕜 (x - y) (z - x) := by
  rw [segment_eq_image'] at h
  rcases h with ⟨θ, ⟨hθ₀, hθ₁⟩, rfl⟩
  simpa only [add_sub_cancel_left, ← sub_sub, sub_smul, one_smul] using
    (SameRay.sameRay_nonneg_smul_left (z - y) hθ₀).nonneg_smul_right (sub_nonneg.2 hθ₁)

Same-Ray Condition for Points in a Closed Segment

Informal description

Let $\mathbb{K}$ be a commutative ring with a partial order and a strict ordered ring structure, and let $E$ be a $\mathbb{K}$-module. For any points $x, y, z \in E$, if $x$ lies in the closed segment $[y -[𝕜] z]$ joining $y$ and $z$, then the vectors $x - y$ and $z - x$ lie on the same ray in $E$.

segment_inter_eq_endpoint_of_linearIndependent_of_ne theorem

 [CommRing 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [NoZeroDivisors 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E}
  (h : LinearIndependent 𝕜 ![x, y]) {s t : 𝕜} (hs : s ≠ t) (c : E) :
  [c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x}

Full source

lemma segment_inter_eq_endpoint_of_linearIndependent_of_ne
    [CommRing 𝕜] [PartialOrder 𝕜] [IsOrderedRing 𝕜] [NoZeroDivisors 𝕜]
    [AddCommGroup E] [Module 𝕜 E]
    {x y : E} (h : LinearIndependent 𝕜 ![x, y]) {s t : 𝕜} (hs : s ≠ t) (c : E) :
    [c + x -[𝕜] c + t • y][c + x -[𝕜] c + t • y] ∩ [c + x -[𝕜] c + s • y] = {c + x} := by
  apply segment_inter_eq_endpoint_of_linearIndependent_sub
  simp only [add_sub_add_left_eq_sub]
  suffices H : LinearIndependent 𝕜 ![(-1 : 𝕜) • x + t • y, (-1 : 𝕜) • x + s • y] by
    convert H using 1; simp only [neg_smul, one_smul]; abel_nf
  nontriviality 𝕜
  rw [LinearIndependent.pair_add_smul_add_smul_iff]
  aesop

Intersection of Segments with Common Endpoint is Exactly the Endpoint under Linear Independence and Distinct Scalars

Informal description

Let $\mathbb{K}$ be a commutative ring with a partial order and an ordered ring structure, and with no zero divisors. Let $E$ be a $\mathbb{K}$-module, and let $x, y \in E$ be linearly independent vectors over $\mathbb{K}$. For any distinct scalars $s, t \in \mathbb{K}$ and any vector $c \in E$, the intersection of the closed segments $[c + x, c + t \cdot y]$ and $[c + x, c + s \cdot y]$ is the singleton set $\{c + x\}$.

midpoint_mem_segment theorem

[Invertible (2 : 𝕜)] (x y : E) : midpoint 𝕜 x y ∈ [x -[𝕜] y]

Full source

theorem midpoint_mem_segment [Invertible (2 : 𝕜)] (x y : E) : midpointmidpoint 𝕜 x y ∈ [x -[𝕜] y] := by
  rw [segment_eq_image_lineMap]
  exact ⟨⅟ 2, ⟨invOf_nonneg.mpr zero_le_two, invOf_le_one one_le_two⟩, rfl⟩

Midpoint Lies in Closed Segment

Informal description

Let $\mathbb{K}$ be a ring with an invertible element $2$, and let $E$ be a $\mathbb{K}$-module. For any two points $x, y \in E$, the midpoint of $x$ and $y$ lies in the closed segment joining $x$ and $y$, i.e., \[ \text{midpoint}_{\mathbb{K}}(x, y) \in [x -[\mathbb{K}] y]. \]

mem_segment_sub_add theorem

[Invertible (2 : 𝕜)] (x y : E) : x ∈ [x - y -[𝕜] x + y]

Full source

theorem mem_segment_sub_add [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x - y -[𝕜] x + y] := by
  convert midpoint_mem_segment (𝕜 := 𝕜) (x - y) (x + y)
  rw [midpoint_sub_add]

Point $x$ lies in the segment between $x - y$ and $x + y$ when $2$ is invertible

Informal description

Let $\mathbb{K}$ be a ring with an invertible element $2$, and let $E$ be a $\mathbb{K}$-module. For any two points $x, y \in E$, the point $x$ lies in the closed segment joining $x - y$ and $x + y$, i.e., \[ x \in [x - y, x + y]. \]

mem_segment_add_sub theorem

[Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y]

Full source

theorem mem_segment_add_sub [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y] := by
  convert midpoint_mem_segment (𝕜 := 𝕜) (x + y) (x - y)
  rw [midpoint_add_sub]

Point Lies in Segment Between Sum and Difference

Informal description

Let $\mathbb{K}$ be a ring with an invertible element $2$, and let $E$ be a $\mathbb{K}$-module. For any two points $x, y \in E$, the point $x$ lies in the closed segment joining $x + y$ and $x - y$, i.e., \[ x \in [x + y -[\mathbb{K}] x - y]. \]

left_mem_openSegment_iff theorem

[DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : x ∈ openSegment 𝕜 x y ↔ x = y

Full source

@[simp]
theorem left_mem_openSegment_iff [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] :
    x ∈ openSegment 𝕜 x yx ∈ openSegment 𝕜 x y ↔ x = y := by
  constructor
  · rintro ⟨a, b, _, hb, hab, hx⟩
    refine smul_right_injective _ hb.ne' ((add_right_inj (a • x)).1 ?_)
    rw [hx, ← add_smul, hab, one_smul]
  · rintro rfl
    rw [openSegment_same]
    exact mem_singleton _

Characterization of Left Endpoint in Open Segment: $x \in \mathopen{]}x, y\mathclose{[} \leftrightarrow x = y$

Informal description

Let $\mathbb{K}$ be a densely ordered field and $E$ be a vector space over $\mathbb{K}$ with no zero scalar multiplication divisors. For any two points $x, y \in E$, the point $x$ belongs to the open segment between $x$ and $y$ if and only if $x = y$.

right_mem_openSegment_iff theorem

[DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] : y ∈ openSegment 𝕜 x y ↔ x = y

Full source

@[simp]
theorem right_mem_openSegment_iff [DenselyOrdered 𝕜] [NoZeroSMulDivisors 𝕜 E] :
    y ∈ openSegment 𝕜 x yy ∈ openSegment 𝕜 x y ↔ x = y := by rw [openSegment_symm, left_mem_openSegment_iff, eq_comm]

Characterization of Right Endpoint in Open Segment: $y \in \mathopen{]}x, y\mathclose{[} \leftrightarrow x = y$

Informal description

Let $\mathbb{K}$ be a densely ordered field and $E$ be a vector space over $\mathbb{K}$ with no zero scalar multiplication divisors. For any two points $x, y \in E$, the point $y$ belongs to the open segment between $x$ and $y$ if and only if $x = y$.

mem_segment_iff_div theorem

 : x ∈ [y -[𝕜] z] ↔ ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Full source

theorem mem_segment_iff_div :
    x ∈ [y -[𝕜] z]x ∈ [y -[𝕜] z] ↔
      ∃ a b : 𝕜, 0 ≤ a ∧ 0 ≤ b ∧ 0 < a + b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x := by
  constructor
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    simp [*]
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
    rw [← add_div, div_self hab.ne']

Characterization of Points in Closed Segment via Non-Negative Weights

Informal description

For any points $x, y, z$ in a $\mathbb{K}$-vector space $E$, the point $x$ belongs to the closed segment between $y$ and $z$ if and only if there exist non-negative scalars $a, b \in \mathbb{K}$ with $a + b > 0$ such that $x = \frac{a}{a + b} \cdot y + \frac{b}{a + b} \cdot z$.

mem_openSegment_iff_div theorem

: x ∈ openSegment 𝕜 y z ↔ ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x

Full source

theorem mem_openSegment_iff_div : x ∈ openSegment 𝕜 y zx ∈ openSegment 𝕜 y z ↔
    ∃ a b : 𝕜, 0 < a ∧ 0 < b ∧ (a / (a + b)) • y + (b / (a + b)) • z = x := by
  constructor
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    use a, b, ha, hb
    rw [hab, div_one, div_one]
  · rintro ⟨a, b, ha, hb, rfl⟩
    have hab : 0 < a + b := add_pos' ha hb
    refine ⟨a / (a + b), b / (a + b), by positivity, by positivity, ?_, rfl⟩
    rw [← add_div, div_self hab.ne']

Characterization of Points in Open Segment via Positive Weights

Informal description

For any points $x, y, z$ in a $\mathbb{K}$-vector space $E$, the point $x$ belongs to the open segment between $y$ and $z$ if and only if there exist positive scalars $a, b \in \mathbb{K}$ such that $x = \frac{a}{a + b} \cdot y + \frac{b}{a + b} \cdot z$.

mem_segment_iff_sameRay theorem

: x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x)

Full source

theorem mem_segment_iff_sameRay : x ∈ [y -[𝕜] z]x ∈ [y -[𝕜] z] ↔ SameRay 𝕜 (x - y) (z - x) := by
  refine ⟨sameRay_of_mem_segment, fun h => ?_⟩
  rcases h.exists_eq_smul_add with ⟨a, b, ha, hb, hab, hxy, hzx⟩
  rw [add_comm, sub_add_sub_cancel] at hxy hzx
  rw [← mem_segment_translate _ (-x), neg_add_cancel]
  refine ⟨b, a, hb, ha, add_comm a b ▸ hab, ?_⟩
  rw [← sub_eq_neg_add, ← neg_sub, hxy, ← sub_eq_neg_add, hzx, smul_neg, smul_comm, neg_add_cancel]

Characterization of Closed Segment Membership via Same-Ray Condition

Informal description

Let $\mathbb{K}$ be a commutative ring with a partial order and a strict ordered ring structure, and let $E$ be a $\mathbb{K}$-module. For any points $x, y, z \in E$, the point $x$ belongs to the closed segment $[y, z]$ if and only if the vectors $x - y$ and $z - x$ lie on the same ray in $E$.

openSegment_subset_union theorem

 (x y : E) {z : E} (hz : z ∈ range (lineMap x y : 𝕜 → E)) :
  openSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y)

Full source

/-- If `z = lineMap x y c` is a point on the line passing through `x` and `y`, then the open
segment `openSegment 𝕜 x y` is included in the union of the open segments `openSegment 𝕜 x z`,
`openSegment 𝕜 z y`, and the point `z`. Informally, `(x, y) ⊆ {z} ∪ (x, z) ∪ (z, y)`. -/
theorem openSegment_subset_union (x y : E) {z : E} (hz : z ∈ range (lineMap x y : 𝕜 → E)) :
    openSegmentopenSegment 𝕜 x y ⊆ insert z (openSegment 𝕜 x z ∪ openSegment 𝕜 z y) := by
  rcases hz with ⟨c, rfl⟩
  simp only [openSegment_eq_image_lineMap, ← mapsTo']
  rintro a ⟨h₀, h₁⟩
  rcases lt_trichotomy a c with (hac | rfl | hca)
  · right
    left
    have hc : 0 < c := h₀.trans hac
    refine ⟨a / c, ⟨div_pos h₀ hc, (div_lt_one hc).2 hac⟩, ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, div_mul_cancel₀ _ hc.ne']
  · left
    rfl
  · right
    right
    have hc : 0 < 1 - c := sub_pos.2 (hca.trans h₁)
    simp only [← lineMap_apply_one_sub y]
    refine
      ⟨(a - c) / (1 - c), ⟨div_pos (sub_pos.2 hca) hc, (div_lt_one hc).2 <| sub_lt_sub_right h₁ _⟩,
        ?_⟩
    simp only [← homothety_eq_lineMap, ← homothety_mul_apply, sub_mul, one_mul,
      div_mul_cancel₀ _ hc.ne', sub_sub_sub_cancel_right]

Open Segment Decomposition along a Line Point

Informal description

For any points $x, y$ in a $\mathbb{K}$-vector space $E$, and any point $z$ lying on the line through $x$ and $y$ (i.e., $z = (1 - \theta)x + \theta y$ for some $\theta \in \mathbb{K}$), the open segment between $x$ and $y$ is contained in the union of the open segments between $x$ and $z$, between $z$ and $y$, and the singleton set $\{z\}$. In other words: \[ \text{openSegment}_{\mathbb{K}}(x, y) \subseteq \{z\} \cup \text{openSegment}_{\mathbb{K}}(x, z) \cup \text{openSegment}_{\mathbb{K}}(z, y). \]

segment_subset_Icc theorem

(h : x ≤ y) : [x -[𝕜] y] ⊆ Icc x y

Full source

theorem segment_subset_Icc (h : x ≤ y) : [x -[𝕜] y][x -[𝕜] y] ⊆ Icc x y := by
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  constructor
  · calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ ≤ a • x + b • y := by gcongr
  · calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _

Inclusion of Segment in Closed Interval: $[x, y] \subseteq \text{Icc}(x, y)$ for $x \leq y$

Informal description

For any two points $x$ and $y$ in an ordered vector space over $\mathbb{K}$ with $x \leq y$, the closed segment $[x, y]$ is contained in the closed interval $\text{Icc}(x, y) = \{z \mid x \leq z \leq y\}$.

openSegment_subset_Ioo theorem

(h : x < y) : openSegment 𝕜 x y ⊆ Ioo x y

Full source

theorem openSegment_subset_Ioo (h : x < y) : openSegmentopenSegment 𝕜 x y ⊆ Ioo x y := by
  rintro z ⟨a, b, ha, hb, hab, rfl⟩
  constructor
  · calc
      x = a • x + b • x := (Convex.combo_self hab _).symm
      _ < a • x + b • y := by gcongr
  · calc
      a • x + b • y < a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _

Open Segment Contained in Open Interval for Ordered Vector Spaces

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any elements $x, y \in E$ with $x < y$, the open segment $\{a \cdot x + b \cdot y \mid a, b \in \mathbb{K}, a, b > 0, a + b = 1\}$ is contained in the open interval $(x, y)$.

segment_subset_uIcc theorem

(x y : E) : [x -[𝕜] y] ⊆ uIcc x y

Full source

theorem segment_subset_uIcc (x y : E) : [x -[𝕜] y][x -[𝕜] y] ⊆ uIcc x y := by
  rcases le_total x y with h | h
  · rw [uIcc_of_le h]
    exact segment_subset_Icc h
  · rw [uIcc_of_ge h, segment_symm]
    exact segment_subset_Icc h

Closed Segment is Subset of Unordered Closed Interval: $[x, y] \subseteq [\min(x, y), \max(x, y)]$

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, the closed segment $[x -[𝕜] y]$ is contained in the unordered closed interval $\text{uIcc}(x, y) = [\min(x, y), \max(x, y)]$.

Convex.min_le_combo theorem

(x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : min x y ≤ a • x + b • y

Full source

theorem Convex.min_le_combo (x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    min x y ≤ a • x + b • y :=
  (segment_subset_uIcc x y ⟨_, _, ha, hb, hab, rfl⟩).1

Lower Bound of Convex Combination by Minimum

Informal description

For any elements $x, y$ in an ordered $\mathbb{K}$-vector space $E$, and nonnegative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ is bounded below by the minimum of $x$ and $y$, i.e., $\min(x, y) \leq a \cdot x + b \cdot y$.

Convex.combo_le_max theorem

(x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) : a • x + b • y ≤ max x y

Full source

theorem Convex.combo_le_max (x y : E) (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • x + b • y ≤ max x y :=
  (segment_subset_uIcc x y ⟨_, _, ha, hb, hab, rfl⟩).2

Convex Combination is Bounded by Maximum: $a \cdot x + b \cdot y \leq \max(x, y)$

Informal description

For any two points $x$ and $y$ in a $\mathbb{K}$-vector space $E$, and for any non-negative scalars $a$ and $b$ such that $a + b = 1$, the convex combination $a \cdot x + b \cdot y$ is less than or equal to the maximum of $x$ and $y$, i.e., $a \cdot x + b \cdot y \leq \max(x, y)$.

Icc_subset_segment theorem

: Icc x y ⊆ [x -[𝕜] y]

Full source

theorem Icc_subset_segment : IccIcc x y ⊆ [x -[𝕜] y] := by
  rintro z ⟨hxz, hyz⟩
  obtain rfl | h := (hxz.trans hyz).eq_or_lt
  · rw [segment_same]
    exact hyz.antisymm hxz
  rw [← sub_nonneg] at hxz hyz
  rw [← sub_pos] at h
  refine ⟨(y - z) / (y - x), (z - x) / (y - x), div_nonneg hyz h.le, div_nonneg hxz h.le, ?_, ?_⟩
  · rw [← add_div, sub_add_sub_cancel, div_self h.ne']
  · rw [smul_eq_mul, smul_eq_mul, ← mul_div_right_comm, ← mul_div_right_comm, ← add_div,
      div_eq_iff h.ne', add_comm, sub_mul, sub_mul, mul_comm x, sub_add_sub_cancel, mul_sub]

Closed Interval is Subset of Closed Segment: $[x, y] \subseteq [x -[\mathbb{K}] y]$

Informal description

For any elements $x$ and $y$ in a $\mathbb{K}$-vector space $E$ with a linear order, the closed interval $[x, y]$ is contained in the closed segment $[x -[\mathbb{K}] y]$.

segment_eq_Icc theorem

(h : x ≤ y) : [x -[𝕜] y] = Icc x y

Full source

@[simp]
theorem segment_eq_Icc (h : x ≤ y) : [x -[𝕜] y] = Icc x y :=
  (segment_subset_Icc h).antisymm Icc_subset_segment

Closed Segment Equals Closed Interval for Ordered Vector Spaces

Informal description

For any two points $x$ and $y$ in an ordered vector space over $\mathbb{K}$ with $x \leq y$, the closed segment $[x -[\mathbb{K}] y]$ is equal to the closed interval $[x, y] = \{z \mid x \leq z \leq y\}$.

Ioo_subset_openSegment theorem

: Ioo x y ⊆ openSegment 𝕜 x y

Full source

theorem Ioo_subset_openSegment : IooIoo x y ⊆ openSegment 𝕜 x y := fun _ hz =>
  mem_openSegment_of_ne_left_right hz.1.ne hz.2.ne' <| Icc_subset_segment <| Ioo_subset_Icc_self hz

Open Interval is Subset of Open Segment: $(x, y) \subseteq \text{openSegment}_{\mathbb{K}}(x, y)$

Informal description

For any elements $x$ and $y$ in a $\mathbb{K}$-vector space $E$ with a linear order, the open interval $(x, y)$ is contained in the open segment between $x$ and $y$, i.e., $\{z \mid x < z < y\} \subseteq \text{openSegment}_{\mathbb{K}}(x, y)$.

openSegment_eq_Ioo theorem

(h : x < y) : openSegment 𝕜 x y = Ioo x y

Full source

@[simp]
theorem openSegment_eq_Ioo (h : x < y) : openSegment 𝕜 x y = Ioo x y :=
  (openSegment_subset_Ioo h).antisymm Ioo_subset_openSegment

Open Segment Equals Open Interval for Ordered Vector Spaces

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any elements $x, y \in E$ with $x < y$, the open segment $\{a \cdot x + b \cdot y \mid a, b \in \mathbb{K}, a, b > 0, a + b = 1\}$ is equal to the open interval $(x, y) = \{z \mid x < z < y\}$.

segment_eq_Icc' theorem

(x y : 𝕜) : [x -[𝕜] y] = Icc (min x y) (max x y)

Full source

theorem segment_eq_Icc' (x y : 𝕜) : [x -[𝕜] y] = Icc (min x y) (max x y) := by
  rcases le_total x y with h | h
  · rw [segment_eq_Icc h, max_eq_right h, min_eq_left h]
  · rw [segment_symm, segment_eq_Icc h, max_eq_left h, min_eq_right h]

Closed Segment Equals Closed Interval of Min and Max

Informal description

For any two elements $x$ and $y$ in an ordered $\mathbb{K}$-vector space, the closed segment $[x -[\mathbb{K}] y]$ is equal to the closed interval $[\min(x, y), \max(x, y)]$.

openSegment_eq_Ioo' theorem

(hxy : x ≠ y) : openSegment 𝕜 x y = Ioo (min x y) (max x y)

Full source

theorem openSegment_eq_Ioo' (hxy : x ≠ y) : openSegment 𝕜 x y = Ioo (min x y) (max x y) := by
  rcases hxy.lt_or_lt with h | h
  · rw [openSegment_eq_Ioo h, max_eq_right h.le, min_eq_left h.le]
  · rw [openSegment_symm, openSegment_eq_Ioo h, max_eq_left h.le, min_eq_right h.le]

Open Segment Equals Open Interval for Distinct Points in Ordered Vector Spaces

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any distinct elements $x, y \in E$, the open segment $\{a \cdot x + b \cdot y \mid a, b \in \mathbb{K}, a, b > 0, a + b = 1\}$ is equal to the open interval $(\min(x, y), \max(x, y))$.

segment_eq_uIcc theorem

(x y : 𝕜) : [x -[𝕜] y] = uIcc x y

Full source

theorem segment_eq_uIcc (x y : 𝕜) : [x -[𝕜] y] = uIcc x y :=
  segment_eq_Icc' _ _

Closed Segment as Unordered Closed Interval

Informal description

For any two elements $x$ and $y$ in an ordered $\mathbb{K}$-vector space, the closed segment $[x -[\mathbb{K}] y]$ is equal to the unordered closed interval $\text{uIcc}(x, y) = [\min(x, y), \max(x, y)]$.

Convex.mem_Icc theorem

(h : x ≤ y) : z ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Full source

/-- A point is in an `Icc` iff it can be expressed as a convex combination of the endpoints. -/
theorem Convex.mem_Icc (h : x ≤ y) :
    z ∈ Icc x yz ∈ Icc x y ↔ ∃ a b, 0 ≤ a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z := by
  simp only [← segment_eq_Icc h, segment, mem_setOf_eq, smul_eq_mul, exists_and_left]

Characterization of Closed Interval Points as Convex Combinations

Informal description

For any two points $x$ and $y$ in an ordered vector space over $\mathbb{K}$ with $x \leq y$, a point $z$ belongs to the closed interval $[x, y]$ if and only if there exist nonnegative scalars $a, b \in \mathbb{K}$ with $a + b = 1$ such that $z = a x + b y$.

Convex.mem_Ioo theorem

(h : x < y) : z ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Full source

/-- A point is in an `Ioo` iff it can be expressed as a strict convex combination of the endpoints.
-/
theorem Convex.mem_Ioo (h : x < y) :
    z ∈ Ioo x yz ∈ Ioo x y ↔ ∃ a b, 0 < a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z := by
  simp only [← openSegment_eq_Ioo h, openSegment, smul_eq_mul, exists_and_left, mem_setOf_eq]

Characterization of Open Interval Points as Strict Convex Combinations

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any elements $x, y \in E$ with $x < y$, a point $z$ belongs to the open interval $(x, y)$ if and only if there exist positive scalars $a, b \in \mathbb{K}$ with $a + b = 1$ such that $z = a x + b y$.

Convex.mem_Ioc theorem

(h : x < y) : z ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z

Full source

/-- A point is in an `Ioc` iff it can be expressed as a semistrict convex combination of the
endpoints. -/
theorem Convex.mem_Ioc (h : x < y) :
    z ∈ Ioc x yz ∈ Ioc x y ↔ ∃ a b, 0 ≤ a ∧ 0 < b ∧ a + b = 1 ∧ a * x + b * y = z := by
  refine ⟨fun hz => ?_, ?_⟩
  · obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ioc_subset_Icc_self hz)
    obtain rfl | hb' := hb.eq_or_lt
    · rw [add_zero] at hab
      rw [hab, one_mul, zero_mul, add_zero] at hz
      exact (hz.1.ne rfl).elim
    · exact ⟨a, b, ha, hb', hab, rfl⟩
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    obtain rfl | ha' := ha.eq_or_lt
    · rw [zero_add] at hab
      rwa [hab, one_mul, zero_mul, zero_add, right_mem_Ioc]
    · exact Ioo_subset_Ioc_self ((Convex.mem_Ioo h).2 ⟨a, b, ha', hb, hab, rfl⟩)

Characterization of Left-Open Right-Closed Interval Points as Semistrict Convex Combinations

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any elements $x, y \in E$ with $x < y$, a point $z$ belongs to the left-open right-closed interval $(x, y]$ if and only if there exist nonnegative scalars $a, b \in \mathbb{K}$ with $0 \leq a$, $0 < b$, $a + b = 1$, such that $z = a x + b y$.

Convex.mem_Ico theorem

(h : x < y) : z ∈ Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z

Full source

/-- A point is in an `Ico` iff it can be expressed as a semistrict convex combination of the
endpoints. -/
theorem Convex.mem_Ico (h : x < y) :
    z ∈ Ico x yz ∈ Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z := by
  refine ⟨fun hz => ?_, ?_⟩
  · obtain ⟨a, b, ha, hb, hab, rfl⟩ := (Convex.mem_Icc h.le).1 (Ico_subset_Icc_self hz)
    obtain rfl | ha' := ha.eq_or_lt
    · rw [zero_add] at hab
      rw [hab, one_mul, zero_mul, zero_add] at hz
      exact (hz.2.ne rfl).elim
    · exact ⟨a, b, ha', hb, hab, rfl⟩
  · rintro ⟨a, b, ha, hb, hab, rfl⟩
    obtain rfl | hb' := hb.eq_or_lt
    · rw [add_zero] at hab
      rwa [hab, one_mul, zero_mul, add_zero, left_mem_Ico]
    · exact Ioo_subset_Ico_self ((Convex.mem_Ioo h).2 ⟨a, b, ha, hb', hab, rfl⟩)

Characterization of Left-Closed Right-Open Interval Points as Semistrict Convex Combinations

Informal description

Let $\mathbb{K}$ be an ordered semiring and $E$ be an ordered $\mathbb{K}$-vector space. For any elements $x, y \in E$ with $x < y$, a point $z$ belongs to the left-closed right-open interval $[x, y)$ if and only if there exist scalars $a, b \in \mathbb{K}$ with $a > 0$, $b \geq 0$, and $a + b = 1$ such that $z = a x + b y$.

Prod.segment_subset theorem

(x y : E × F) : segment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2

Full source

theorem segment_subset (x y : E × F) : segmentsegment 𝕜 x y ⊆ segment 𝕜 x.1 y.1 ×ˢ segment 𝕜 x.2 y.2 := by
  rintro z ⟨a, b, ha, hb, hab, hz⟩
  exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Product Segment Subset Property

Informal description

For any pair of points $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product space $E \times F$, the closed segment joining $x$ and $y$ is contained in the Cartesian product of the closed segments joining $x_1$ and $y_1$ in $E$ and $x_2$ and $y_2$ in $F$. That is, $$ [x -[𝕜] y] \subseteq [x_1 -[𝕜] y_1] \times [x_2 -[𝕜] y_2]. $$

Prod.openSegment_subset theorem

(x y : E × F) : openSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2

Full source

theorem openSegment_subset (x y : E × F) :
    openSegmentopenSegment 𝕜 x y ⊆ openSegment 𝕜 x.1 y.1 ×ˢ openSegment 𝕜 x.2 y.2 := by
  rintro z ⟨a, b, ha, hb, hab, hz⟩
  exact ⟨⟨a, b, ha, hb, hab, congr_arg Prod.fst hz⟩, a, b, ha, hb, hab, congr_arg Prod.snd hz⟩

Open Segment in Product Space is Subset of Product of Component Open Segments

Informal description

For any two points $x = (x_1, x_2)$ and $y = (y_1, y_2)$ in the product space $E \times F$, the open segment between $x$ and $y$ is contained in the Cartesian product of the open segments between their respective components. That is, for any scalar field $\mathbb{K}$, \[ \text{openSegment}_{\mathbb{K}}(x, y) \subseteq \text{openSegment}_{\mathbb{K}}(x_1, y_1) \times \text{openSegment}_{\mathbb{K}}(x_2, y_2). \]

Prod.image_mk_segment_left theorem

(x₁ x₂ : E) (y : F) : (fun x => (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)]

Full source

theorem image_mk_segment_left (x₁ x₂ : E) (y : F) :
    (fun x => (x, y)) '' [x₁ -[𝕜] x₂] = [(x₁, y) -[𝕜] (x₂, y)] := by
  rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Image of Closed Segment under Left Injection in Product Space

Informal description

For any points $x_1, x_2$ in a $\mathbb{K}$-vector space $E$ and any point $y$ in a $\mathbb{K}$-vector space $F$, the image of the closed segment $[x_1 -[𝕜] x_2]$ under the mapping $x \mapsto (x, y)$ is equal to the closed segment $[(x_1, y) -[𝕜] (x_2, y)]$ in the product space $E \times F$.

Prod.image_mk_segment_right theorem

(x : E) (y₁ y₂ : F) : (fun y => (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)]

Full source

theorem image_mk_segment_right (x : E) (y₁ y₂ : F) :
    (fun y => (x, y)) '' [y₁ -[𝕜] y₂] = [(x, y₁) -[𝕜] (x, y₂)] := by
  rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Image of Closed Segment under Right Projection in Product Space

Informal description

For any fixed point $x$ in a $\mathbb{K}$-vector space $E$ and any two points $y_1, y_2$ in a $\mathbb{K}$-vector space $F$, the image of the closed segment $[y_1 -[𝕜] y_2]$ under the mapping $y \mapsto (x, y)$ equals the closed segment $[(x, y_1) -[𝕜] (x, y_2)]$ in the product space $E × F$. In mathematical notation: $$\{x\} × [y_1 -[𝕜] y_2] = [(x, y_1) -[𝕜] (x, y_2)]$$

Prod.image_mk_openSegment_left theorem

(x₁ x₂ : E) (y : F) : (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y)

Full source

theorem image_mk_openSegment_left (x₁ x₂ : E) (y : F) :
    (fun x => (x, y)) '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (x₁, y) (x₂, y) := by
  rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Preservation of Open Segment under First Component Mapping in Product Space

Informal description

For any points $x_1, x_2$ in a $\mathbb{K}$-vector space $E$ and any point $y$ in a $\mathbb{K}$-vector space $F$, the image of the open segment between $x_1$ and $x_2$ under the function $x \mapsto (x, y)$ is equal to the open segment between $(x_1, y)$ and $(x_2, y)$ in the product space $E \times F$. In other words, the mapping preserves open segments in the first component when paired with a fixed point in the second component.

Prod.image_mk_openSegment_right theorem

(x : E) (y₁ y₂ : F) : (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂)

Full source

@[simp]
theorem image_mk_openSegment_right (x : E) (y₁ y₂ : F) :
    (fun y => (x, y)) '' openSegment 𝕜 y₁ y₂ = openSegment 𝕜 (x, y₁) (x, y₂) := by
  rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp [Convex.combo_self ha.2.2]

Image of Open Segment under Right Projection in Product Space

Informal description

For any fixed element $x$ in a $\mathbb{K}$-vector space $E$ and any two elements $y_1, y_2$ in a $\mathbb{K}$-vector space $F$, the image of the open segment between $y_1$ and $y_2$ under the mapping $y \mapsto (x, y)$ is equal to the open segment between $(x, y_1)$ and $(x, y_2)$ in the product space $E \times F$. In other words: \[ \{(x, y) \mid y \in \text{openSegment}_{\mathbb{K}}(y_1, y_2)\} = \text{openSegment}_{\mathbb{K}}((x, y_1), (x, y_2)). \]

Pi.segment_subset theorem

(x y : ∀ i, M i) : segment 𝕜 x y ⊆ s.pi fun i => segment 𝕜 (x i) (y i)

Full source

theorem segment_subset (x y : ∀ i, M i) : segmentsegment 𝕜 x y ⊆ s.pi fun i => segment 𝕜 (x i) (y i) := by
  rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

Product Space Segment Inclusion: $[x, y] \subseteq \prod_{i \in s} [x_i, y_i]$

Informal description

For any two functions $x, y \in \prod_{i} M_i$ in a product space, the closed segment $[x, y]$ joining $x$ and $y$ is contained in the product of the closed segments $[x_i, y_i]$ for each component $i \in s$. That is, for any $z \in [x, y]$, we have $z_i \in [x_i, y_i]$ for all $i \in s$.

Pi.openSegment_subset theorem

(x y : ∀ i, M i) : openSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i)

Full source

theorem openSegment_subset (x y : ∀ i, M i) :
    openSegmentopenSegment 𝕜 x y ⊆ s.pi fun i => openSegment 𝕜 (x i) (y i) := by
  rintro z ⟨a, b, ha, hb, hab, hz⟩ i -
  exact ⟨a, b, ha, hb, hab, congr_fun hz i⟩

Open Segment in Product Space is Contained in Product of Open Segments

Informal description

For any family of points $x, y \in \prod_{i} M_i$ in a product of $\mathbb{K}$-vector spaces, the open segment between $x$ and $y$ is contained in the product of the open segments between their components. That is, for any index set $s \subseteq \iota$, we have: \[ \text{openSegment}_{\mathbb{K}}(x, y) \subseteq \prod_{i \in s} \text{openSegment}_{\mathbb{K}}(x_i, y_i). \]

Pi.image_update_segment theorem

 (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) : update y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂]

Full source

theorem image_update_segment (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) :
    updateupdate y i '' [x₁ -[𝕜] x₂] = [update y i x₁ -[𝕜] update y i x₂] := by
  rw [segment_eq_image₂, segment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Image of Closed Segment under Function Update Equals Closed Segment of Updated Functions

Informal description

For any index $i$ in an index set $\iota$, any two points $x_1, x_2$ in a $\mathbb{K}$-vector space $M_i$, and any function $y \colon \iota \to \bigcup_{i} M_i$, the image of the closed segment $[x_1, x_2]$ under the function update $\text{update } y \, i$ is equal to the closed segment between the updated functions $\text{update } y \, i \, x_1$ and $\text{update } y \, i \, x_2$. That is: \[ \text{update } y \, i \big( [x_1, x_2] \big) = [\text{update } y \, i \, x_1, \text{update } y \, i \, x_2]. \]

Pi.image_update_openSegment theorem

 (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) :
  update y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂)

Full source

theorem image_update_openSegment (i : ι) (x₁ x₂ : M i) (y : ∀ i, M i) :
    updateupdate y i '' openSegment 𝕜 x₁ x₂ = openSegment 𝕜 (update y i x₁) (update y i x₂) := by
  rw [openSegment_eq_image₂, openSegment_eq_image₂, image_image]
  refine EqOn.image_eq fun a ha ↦ ?_
  simp only [← update_smul, ← update_add, Convex.combo_self ha.2.2]

Image of Open Segment under Function Update Equals Open Segment of Updated Points

Informal description

Let $E$ be a $\mathbb{K}$-vector space, and let $x_1, x_2 \in E$ and $y \in \prod_{i \in \iota} E$ be given. For any index $i \in \iota$, the image of the open segment $\text{openSegment}_{\mathbb{K}}(x_1, x_2)$ under the function update $y \mapsto \text{update } y \, i$ is equal to the open segment between the updated points: \[ \text{update } y \, i \left( \text{openSegment}_{\mathbb{K}}(x_1, x_2) \right) = \text{openSegment}_{\mathbb{K}}(\text{update } y \, i \, x_1, \text{update } y \, i \, x_2). \] Here, $\text{update } y \, i \, x$ denotes the function that coincides with $y$ everywhere except at index $i$, where it takes the value $x$.

Mathlib.Analysis.Convex.Segment

Notations

TODO