Mathlib.LinearAlgebra.AffineSpace.Midpoint

midpoint definition

(x y : P) : P

Full source

/-- `midpoint x y` is the midpoint of the segment `[x, y]`. -/
def midpoint (x y : P) : P :=
  lineMap x y (⅟ 2 : R)

Midpoint of two points in an affine space

Informal description

Given a ring $R$ with an invertible element $2$ and an affine space $P$ over $R$, the midpoint of two points $x, y \in P$ is defined as the affine combination $\frac{1}{2}x + \frac{1}{2}y$, where $\frac{1}{2}$ denotes the multiplicative inverse of $2$ in $R$.

AffineMap.map_midpoint theorem

(f : P →ᵃ[R] P') (a b : P) : f (midpoint R a b) = midpoint R (f a) (f b)

Full source

@[simp]
theorem AffineMap.map_midpoint (f : P →ᵃ[R] P') (a b : P) :
    f (midpoint R a b) = midpoint R (f a) (f b) :=
  f.apply_lineMap a b _

Affine Maps Preserve Midpoints

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ and $P'$ be affine spaces over $R$. For any affine map $f \colon P \to P'$ and any two points $a, b \in P$, the image of the midpoint of $a$ and $b$ under $f$ is equal to the midpoint of $f(a)$ and $f(b)$, i.e., $$ f\left(\text{midpoint}_R(a, b)\right) = \text{midpoint}_R(f(a), f(b)). $$

AffineEquiv.map_midpoint theorem

(f : P ≃ᵃ[R] P') (a b : P) : f (midpoint R a b) = midpoint R (f a) (f b)

Full source

@[simp]
theorem AffineEquiv.map_midpoint (f : P ≃ᵃ[R] P') (a b : P) :
    f (midpoint R a b) = midpoint R (f a) (f b) :=
  f.apply_lineMap a b _

Affine Equivalence Preserves Midpoints

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ and $P'$ be affine spaces over $R$. For any affine equivalence $f \colon P \simeqᵃ[R] P'$ and any points $a, b \in P$, the image of the midpoint of $a$ and $b$ under $f$ is equal to the midpoint of $f(a)$ and $f(b)$ in $P'$. That is, $$ f(\text{midpoint}_R(a, b)) = \text{midpoint}_R(f(a), f(b)). $$

AffineEquiv.pointReflection_midpoint_left theorem

(x y : P) : pointReflection R (midpoint R x y) x = y

Full source

theorem AffineEquiv.pointReflection_midpoint_left (x y : P) :
    pointReflection R (midpoint R x y) x = y := by
  rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

Point Reflection Property: $\text{pointReflection}_{\text{midpoint}(x,y)}(x) = y$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a ring $R$ with invertible $2$, the point reflection of $x$ about the midpoint of $x$ and $y$ equals $y$. That is, if $m$ is the midpoint of $x$ and $y$, then the point reflection $\text{pointReflection}_m(x) = y$.

Equiv.pointReflection_midpoint_left theorem

(x y : P) : (Equiv.pointReflection (midpoint R x y)) x = y

Full source

@[simp]
theorem Equiv.pointReflection_midpoint_left (x y : P) :
    (Equiv.pointReflection (midpoint R x y)) x = y := by
  rw [midpoint, pointReflection_apply, lineMap_apply, vadd_vsub, vadd_vadd, ← add_smul, ← two_mul,
    mul_invOf_self, one_smul, vsub_vadd]

Point Reflection about Midpoint Swaps Points: $\text{pointReflection}(\text{midpoint}(x, y))(x) = y$

Informal description

Let $P$ be an affine space over a ring $R$ with an invertible element $2$. For any two points $x, y \in P$, the point reflection of $x$ about the midpoint of $x$ and $y$ equals $y$, i.e., \[ \text{pointReflection}(\text{midpoint}(x, y))(x) = y. \]

midpoint_comm theorem

(x y : P) : midpoint R x y = midpoint R y x

Full source

theorem midpoint_comm (x y : P) : midpoint R x y = midpoint R y x := by
  rw [midpoint, ← lineMap_apply_one_sub, one_sub_invOf_two, midpoint]

Commutativity of Midpoint: $\text{midpoint}(x, y) = \text{midpoint}(y, x)$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a ring $R$ with invertible $2$, the midpoint of $x$ and $y$ is equal to the midpoint of $y$ and $x$, i.e., \[ \text{midpoint}(x, y) = \text{midpoint}(y, x). \]

AffineEquiv.pointReflection_midpoint_right theorem

(x y : P) : pointReflection R (midpoint R x y) y = x

Full source

theorem AffineEquiv.pointReflection_midpoint_right (x y : P) :
    pointReflection R (midpoint R x y) y = x := by
  rw [midpoint_comm, AffineEquiv.pointReflection_midpoint_left]

Point Reflection Property: $\text{pointReflection}_{\text{midpoint}(x,y)}(y) = x$

Informal description

For any points $x$ and $y$ in an affine space $P$ over a ring $R$ with invertible $2$, the point reflection of $y$ about the midpoint of $x$ and $y$ equals $x$. That is, if $m$ is the midpoint of $x$ and $y$, then the point reflection $\text{pointReflection}_m(y) = x$.

Equiv.pointReflection_midpoint_right theorem

(x y : P) : (Equiv.pointReflection (midpoint R x y)) y = x

Full source

@[simp]
theorem Equiv.pointReflection_midpoint_right (x y : P) :
    (Equiv.pointReflection (midpoint R x y)) y = x := by
  rw [midpoint_comm, Equiv.pointReflection_midpoint_left]

Point Reflection about Midpoint Swaps Points: $\text{pointReflection}(\text{midpoint}(x, y))(y) = x$

Informal description

Let $P$ be an affine space over a ring $R$ with an invertible element $2$. For any two points $x, y \in P$, the point reflection of $y$ about the midpoint of $x$ and $y$ equals $x$, i.e., \[ \text{pointReflection}(\text{midpoint}(x, y))(y) = x. \]

midpoint_vsub_midpoint theorem

 (p₁ p₂ p₃ p₄ : P) : midpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)

Full source

theorem midpoint_vsub_midpoint (p₁ p₂ p₃ p₄ : P) :
    midpointmidpoint R p₁ p₂ -ᵥ midpoint R p₃ p₄ = midpoint R (p₁ -ᵥ p₃) (p₂ -ᵥ p₄) :=
  lineMap_vsub_lineMap _ _ _ _ _

Midpoint of Vector Differences Equals Vector Difference of Midpoints

Informal description

Let $P$ be an affine space over a ring $R$ with invertible $2$. For any four points $p_1, p_2, p_3, p_4 \in P$, the vector difference between their midpoints equals the midpoint of their vector differences: $$ \text{midpoint}(p_1, p_2) - \text{midpoint}(p_3, p_4) = \text{midpoint}(p_1 - p_3, p_2 - p_4). $$

midpoint_vadd_midpoint theorem

(v v' : V) (p p' : P) : midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')

Full source

theorem midpoint_vadd_midpoint (v v' : V) (p p' : P) :
    midpointmidpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p') :=
  lineMap_vadd_lineMap _ _ _ _ _

Midpoint Addition Formula: $\text{midpoint}(v, v') + \text{midpoint}(p, p') = \text{midpoint}(v + p, v' + p')$

Informal description

Let $V$ be a vector space and $P$ an affine space over a ring $R$ with invertible $2$. For any vectors $v, v' \in V$ and points $p, p' \in P$, the sum of the midpoint of $v$ and $v'$ with the midpoint of $p$ and $p'$ equals the midpoint of the translated points $v + p$ and $v' + p'$. In other words, $$ \text{midpoint}(v, v') + \text{midpoint}(p, p') = \text{midpoint}(v + p, v' + p'). $$

midpoint_eq_iff theorem

{x y z : P} : midpoint R x y = z ↔ pointReflection R z x = y

Full source

theorem midpoint_eq_iff {x y z : P} : midpointmidpoint R x y = z ↔ pointReflection R z x = y :=
  eq_comm.trans
    ((injective_pointReflection_left_of_module R x).eq_iff'
        (AffineEquiv.pointReflection_midpoint_left x y)).symm

Midpoint Characterization via Point Reflection

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y, z \in P$, the point $z$ is the midpoint of $x$ and $y$ if and only if the point reflection of $x$ about $z$ equals $y$, i.e., \[ z = \text{midpoint}_R(x, y) \iff \text{pointReflection}_R(z)(x) = y. \]

midpoint_pointReflection_left theorem

(x y : P) : midpoint R (Equiv.pointReflection x y) y = x

Full source

@[simp]
theorem midpoint_pointReflection_left (x y : P) :
    midpoint R (Equiv.pointReflection x y) y = x :=
  midpoint_eq_iff.2 <| Equiv.pointReflection_involutive _ _

Midpoint of Point Reflection and Original Point Equals Center

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of the point reflection of $y$ about $x$ and $y$ is equal to $x$, i.e., \[ \text{midpoint}_R(\text{pointReflection}_R(x)(y), y) = x. \]

midpoint_pointReflection_right theorem

(x y : P) : midpoint R y (Equiv.pointReflection x y) = x

Full source

@[simp]
theorem midpoint_pointReflection_right (x y : P) :
    midpoint R y (Equiv.pointReflection x y) = x :=
  midpoint_eq_iff.2 rfl

Midpoint of Point and Its Reflection Equals Center Point

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of $y$ and the point reflection of $y$ about $x$ is equal to $x$, i.e., \[ \text{midpoint}_R(y, \text{pointReflection}_R(x)(y)) = x. \]

AffineEquiv.midpoint_pointReflection_left theorem

(x y : P) : midpoint R (pointReflection R x y) y = x

Full source

nonrec lemma AffineEquiv.midpoint_pointReflection_left (x y : P) :
    midpoint R (pointReflection R x y) y = x :=
  midpoint_pointReflection_left x y

Midpoint of Reflection and Original Point Equals Center

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of the point reflection of $y$ about $x$ and $y$ is equal to $x$, i.e., \[ \text{midpoint}_R(\text{pointReflection}_R(x)(y), y) = x. \]

AffineEquiv.midpoint_pointReflection_right theorem

(x y : P) : midpoint R y (pointReflection R x y) = x

Full source

nonrec lemma AffineEquiv.midpoint_pointReflection_right (x y : P) :
    midpoint R y (pointReflection R x y) = x :=
  midpoint_pointReflection_right x y

Midpoint of Point and Its Reflection Equals Center Point

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of $y$ and the point reflection of $y$ about $x$ is equal to $x$, i.e., \[ \text{midpoint}_R(y, \text{pointReflection}_R(x)(y)) = x. \]

midpoint_vsub_left theorem

(p₁ p₂ : P) : midpoint R p₁ p₂ -ᵥ p₁ = (⅟ 2 : R) • (p₂ -ᵥ p₁)

Full source

@[simp]
theorem midpoint_vsub_left (p₁ p₂ : P) : midpointmidpoint R p₁ p₂ -ᵥ p₁ = (⅟ 2 : R) • (p₂ -ᵥ p₁) :=
  lineMap_vsub_left _ _ _

Vector Difference Between Midpoint and Left Point

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a ring $R$ with invertible $2$, the vector difference between the midpoint of $p_1$ and $p_2$ and $p_1$ is equal to the inverse of $2$ in $R$ multiplied by the vector difference between $p_2$ and $p_1$, i.e., \[ \text{midpoint}(p_1, p_2) - p_1 = \frac{1}{2} (p_2 - p_1). \]

midpoint_vsub_right theorem

(p₁ p₂ : P) : midpoint R p₁ p₂ -ᵥ p₂ = (⅟ 2 : R) • (p₁ -ᵥ p₂)

Full source

@[simp]
theorem midpoint_vsub_right (p₁ p₂ : P) : midpointmidpoint R p₁ p₂ -ᵥ p₂ = (⅟ 2 : R) • (p₁ -ᵥ p₂) := by
  rw [midpoint_comm, midpoint_vsub_left]

Vector Difference Between Midpoint and Right Point: $\text{midpoint}(p_1, p_2) - p_2 = \frac{1}{2}(p_1 - p_2)$

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a ring $R$ with invertible $2$, the vector difference between the midpoint of $p_1$ and $p_2$ and $p_2$ is equal to the inverse of $2$ in $R$ multiplied by the vector difference between $p_1$ and $p_2$, i.e., \[ \text{midpoint}(p_1, p_2) - p_2 = \frac{1}{2} (p_1 - p_2). \]

left_vsub_midpoint theorem

(p₁ p₂ : P) : p₁ -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p₁ -ᵥ p₂)

Full source

@[simp]
theorem left_vsub_midpoint (p₁ p₂ : P) : p₁ -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p₁ -ᵥ p₂) :=
  left_vsub_lineMap _ _ _

Vector Difference Between Point and Midpoint

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a ring $R$ with invertible $2$, the vector difference between $p_1$ and the midpoint of $p_1$ and $p_2$ is equal to half the vector difference between $p_1$ and $p_2$, i.e., \[ p_1 - \text{midpoint}(p_1, p_2) = \frac{1}{2} (p_1 - p_2). \]

right_vsub_midpoint theorem

(p₁ p₂ : P) : p₂ -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p₂ -ᵥ p₁)

Full source

@[simp]
theorem right_vsub_midpoint (p₁ p₂ : P) : p₂ -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p₂ -ᵥ p₁) := by
  rw [midpoint_comm, left_vsub_midpoint]

Vector Difference Between Second Point and Midpoint: $p_2 - \text{midpoint}(p_1, p_2) = \frac{1}{2}(p_2 - p_1)$

Informal description

For any two points $p_1$ and $p_2$ in an affine space $P$ over a ring $R$ with invertible $2$, the vector difference between $p_2$ and the midpoint of $p_1$ and $p_2$ is equal to half the vector difference between $p_2$ and $p_1$, i.e., \[ p_2 - \text{midpoint}(p_1, p_2) = \frac{1}{2} (p_2 - p_1). \]

midpoint_vsub theorem

(p₁ p₂ p : P) : midpoint R p₁ p₂ -ᵥ p = (⅟ 2 : R) • (p₁ -ᵥ p) + (⅟ 2 : R) • (p₂ -ᵥ p)

Full source

theorem midpoint_vsub (p₁ p₂ p : P) :
    midpointmidpoint R p₁ p₂ -ᵥ p = (⅟ 2 : R) • (p₁ -ᵥ p) + (⅟ 2 : R) • (p₂ -ᵥ p) := by
  rw [← vsub_sub_vsub_cancel_right p₁ p p₂, smul_sub, sub_eq_add_neg, ← smul_neg,
    neg_vsub_eq_vsub_rev, add_assoc, invOf_two_smul_add_invOf_two_smul, ← vadd_vsub_assoc,
    midpoint_comm, midpoint, lineMap_apply]

Midpoint Vector Difference Formula: $\text{midpoint}(p_1, p_2) - p = \frac{1}{2}(p_1 - p) + \frac{1}{2}(p_2 - p)$

Informal description

Let $P$ be an affine space over a ring $R$ with invertible $2$. For any points $p_1, p_2, p \in P$, the vector difference between the midpoint of $p_1$ and $p_2$ and $p$ is equal to the sum of half the vector difference between $p_1$ and $p$ and half the vector difference between $p_2$ and $p$, i.e., \[ \text{midpoint}(p_1, p_2) - p = \frac{1}{2} (p_1 - p) + \frac{1}{2} (p_2 - p). \]

vsub_midpoint theorem

(p₁ p₂ p : P) : p -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p -ᵥ p₁) + (⅟ 2 : R) • (p -ᵥ p₂)

Full source

theorem vsub_midpoint (p₁ p₂ p : P) :
    p -ᵥ midpoint R p₁ p₂ = (⅟ 2 : R) • (p -ᵥ p₁) + (⅟ 2 : R) • (p -ᵥ p₂) := by
  rw [← neg_vsub_eq_vsub_rev, midpoint_vsub, neg_add, ← smul_neg, ← smul_neg, neg_vsub_eq_vsub_rev,
    neg_vsub_eq_vsub_rev]

Vector Difference from Point to Midpoint Formula: $p - \text{midpoint}(p_1, p_2) = \frac{1}{2}(p - p_1) + \frac{1}{2}(p - p_2)$

Informal description

Let $P$ be an affine space over a ring $R$ with invertible $2$. For any points $p_1, p_2, p \in P$, the vector difference between $p$ and the midpoint of $p_1$ and $p_2$ is equal to the sum of half the vector difference between $p$ and $p_1$ and half the vector difference between $p$ and $p_2$, i.e., \[ p - \text{midpoint}(p_1, p_2) = \frac{1}{2} (p - p_1) + \frac{1}{2} (p - p_2). \]

midpoint_sub_left theorem

(v₁ v₂ : V) : midpoint R v₁ v₂ - v₁ = (⅟ 2 : R) • (v₂ - v₁)

Full source

@[simp]
theorem midpoint_sub_left (v₁ v₂ : V) : midpoint R v₁ v₂ - v₁ = (⅟ 2 : R) • (v₂ - v₁) :=
  midpoint_vsub_left v₁ v₂

Midpoint Difference Identity: $\text{midpoint}(v_1, v_2) - v_1 = \frac{1}{2}(v_2 - v_1)$

Informal description

For any vectors $v_1$ and $v_2$ in a vector space $V$ over a ring $R$ with invertible $2$, the difference between the midpoint of $v_1$ and $v_2$ and $v_1$ is equal to half the difference between $v_2$ and $v_1$, i.e., \[ \text{midpoint}(v_1, v_2) - v_1 = \frac{1}{2} (v_2 - v_1). \]

midpoint_sub_right theorem

(v₁ v₂ : V) : midpoint R v₁ v₂ - v₂ = (⅟ 2 : R) • (v₁ - v₂)

Full source

@[simp]
theorem midpoint_sub_right (v₁ v₂ : V) : midpoint R v₁ v₂ - v₂ = (⅟ 2 : R) • (v₁ - v₂) :=
  midpoint_vsub_right v₁ v₂

Midpoint Difference Identity: $\text{midpoint}(v_1, v_2) - v_2 = \frac{1}{2}(v_1 - v_2)$

Informal description

For any vectors $v_1$ and $v_2$ in a vector space $V$ over a ring $R$ with invertible $2$, the difference between the midpoint of $v_1$ and $v_2$ and $v_2$ is equal to half the difference between $v_1$ and $v_2$, i.e., \[ \text{midpoint}(v_1, v_2) - v_2 = \frac{1}{2} (v_1 - v_2). \]

left_sub_midpoint theorem

(v₁ v₂ : V) : v₁ - midpoint R v₁ v₂ = (⅟ 2 : R) • (v₁ - v₂)

Full source

@[simp]
theorem left_sub_midpoint (v₁ v₂ : V) : v₁ - midpoint R v₁ v₂ = (⅟ 2 : R) • (v₁ - v₂) :=
  left_vsub_midpoint v₁ v₂

Left Difference from Midpoint Identity: $v_1 - \text{midpoint}(v_1, v_2) = \frac{1}{2}(v_1 - v_2)$

Informal description

For any vectors $v_1$ and $v_2$ in a vector space $V$ over a ring $R$ with invertible $2$, the difference between $v_1$ and the midpoint of $v_1$ and $v_2$ is equal to half the difference between $v_1$ and $v_2$, i.e., \[ v_1 - \text{midpoint}(v_1, v_2) = \frac{1}{2} (v_1 - v_2). \]

right_sub_midpoint theorem

(v₁ v₂ : V) : v₂ - midpoint R v₁ v₂ = (⅟ 2 : R) • (v₂ - v₁)

Full source

@[simp]
theorem right_sub_midpoint (v₁ v₂ : V) : v₂ - midpoint R v₁ v₂ = (⅟ 2 : R) • (v₂ - v₁) :=
  right_vsub_midpoint v₁ v₂

Right Difference from Midpoint Identity: $v_2 - \text{midpoint}(v_1, v_2) = \frac{1}{2}(v_2 - v_1)$

Informal description

For any vectors $v_1$ and $v_2$ in a vector space $V$ over a ring $R$ with invertible $2$, the difference between $v_2$ and the midpoint of $v_1$ and $v_2$ is equal to half the difference between $v_2$ and $v_1$, i.e., \[ v_2 - \text{midpoint}_R(v_1, v_2) = \frac{1}{2} (v_2 - v_1). \]

midpoint_eq_left_iff theorem

{x y : P} : midpoint R x y = x ↔ x = y

Full source

@[simp]
theorem midpoint_eq_left_iff {x y : P} : midpointmidpoint R x y = x ↔ x = y := by
  rw [midpoint_eq_iff, pointReflection_self]

Midpoint Equals Left Point if and only if Points are Equal

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of $x$ and $y$ equals $x$ if and only if $x$ equals $y$. In other words, \[ \text{midpoint}_R(x, y) = x \iff x = y. \]

left_eq_midpoint_iff theorem

{x y : P} : x = midpoint R x y ↔ x = y

Full source

@[simp]
theorem left_eq_midpoint_iff {x y : P} : x = midpoint R x y ↔ x = y := by
  rw [eq_comm, midpoint_eq_left_iff]

Left Point Equals Midpoint if and only if Points are Equal

Informal description

For any points $x, y$ in an affine space $P$ over a ring $R$ with invertible $2$, the equality $x = \text{midpoint}_R(x, y)$ holds if and only if $x = y$.

midpoint_eq_right_iff theorem

{x y : P} : midpoint R x y = y ↔ x = y

Full source

@[simp]
theorem midpoint_eq_right_iff {x y : P} : midpointmidpoint R x y = y ↔ x = y := by
  rw [midpoint_comm, midpoint_eq_left_iff, eq_comm]

Midpoint Equals Right Point if and only if Points are Equal

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y \in P$, the midpoint of $x$ and $y$ equals $y$ if and only if $x$ equals $y$. In other words, \[ \text{midpoint}_R(x, y) = y \iff x = y. \]

right_eq_midpoint_iff theorem

{x y : P} : y = midpoint R x y ↔ x = y

Full source

@[simp]
theorem right_eq_midpoint_iff {x y : P} : y = midpoint R x y ↔ x = y := by
  rw [eq_comm, midpoint_eq_right_iff]

Right Point Equals Midpoint if and only if Points are Equal

Informal description

For any points $x, y$ in an affine space $P$ over a ring $R$ with invertible $2$, the equality $y = \text{midpoint}_R(x, y)$ holds if and only if $x = y$.

midpoint_eq_midpoint_iff_vsub_eq_vsub theorem

{x x' y y' : P} : midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y

Full source

theorem midpoint_eq_midpoint_iff_vsub_eq_vsub {x x' y y' : P} :
    midpointmidpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y := by
  rw [← @vsub_eq_zero_iff_eq V, midpoint_vsub_midpoint, midpoint_eq_iff, pointReflection_apply,
    vsub_eq_sub, zero_sub, vadd_eq_add, add_zero, neg_eq_iff_eq_neg, neg_vsub_eq_vsub_rev]

Midpoint Equality Condition via Vector Differences

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any four points $x, x', y, y' \in P$, the midpoints of the segments $[x, y]$ and $[x', y']$ are equal if and only if the vector difference $x - x'$ equals the vector difference $y' - y$. That is, \[ \text{midpoint}_R(x, y) = \text{midpoint}_R(x', y') \iff x - x' = y' - y. \]

midpoint_eq_iff' theorem

{x y z : P} : midpoint R x y = z ↔ Equiv.pointReflection z x = y

Full source

theorem midpoint_eq_iff' {x y z : P} : midpointmidpoint R x y = z ↔ Equiv.pointReflection z x = y :=
  midpoint_eq_iff

Midpoint Characterization via Point Reflection

Informal description

Let $R$ be a ring with an invertible element $2$, and let $P$ be an affine space over $R$. For any points $x, y, z \in P$, the point $z$ is the midpoint of $x$ and $y$ if and only if the point reflection of $x$ about $z$ equals $y$, i.e., \[ z = \text{midpoint}_R(x, y) \iff \text{pointReflection}(z)(x) = y. \]

midpoint_unique theorem

(R' : Type*) [Ring R'] [Invertible (2 : R')] [Module R' V] (x y : P) : midpoint R x y = midpoint R' x y

Full source

/-- `midpoint` does not depend on the ring `R`. -/
theorem midpoint_unique (R' : Type*) [Ring R'] [Invertible (2 : R')] [Module R' V] (x y : P) :
    midpoint R x y = midpoint R' x y :=
  (midpoint_eq_iff' R).2 <| (midpoint_eq_iff' R').1 rfl

Independence of Midpoint Definition from Base Ring

Informal description

Let $R$ and $R'$ be rings with invertible elements $2$, and let $P$ be an affine space over both $R$ and $R'$. For any points $x, y \in P$, the midpoint of $x$ and $y$ defined over $R$ is equal to the midpoint defined over $R'$, i.e., \[ \text{midpoint}_R(x, y) = \text{midpoint}_{R'}(x, y). \]

midpoint_self theorem

(x : P) : midpoint R x x = x

Full source

@[simp]
theorem midpoint_self (x : P) : midpoint R x x = x :=
  lineMap_same_apply _ _

Midpoint of a Point with Itself is the Point Itself

Informal description

For any point $x$ in an affine space $P$ over a ring $R$ with invertible $2$, the midpoint of $x$ and $x$ is equal to $x$ itself, i.e., $\text{midpoint}_R(x, x) = x$.

midpoint_add_self theorem

(x y : V) : midpoint R x y + midpoint R x y = x + y

Full source

@[simp]
theorem midpoint_add_self (x y : V) : midpoint R x y + midpoint R x y = x + y :=
  calc
    midpointmidpoint R x y +ᵥ midpoint R x y = midpointmidpoint R x y +ᵥ midpoint R y x := by rw [midpoint_comm]
    _ = x + y := by rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]

Midpoint Addition Identity: $\text{midpoint}(x,y) + \text{midpoint}(x,y) = x + y$

Informal description

For any vectors $x$ and $y$ in a module $V$ over a ring $R$ with invertible $2$, the sum of the midpoint of $x$ and $y$ with itself equals the sum of $x$ and $y$, i.e., \[ \text{midpoint}_R(x, y) + \text{midpoint}_R(x, y) = x + y. \]

midpoint_zero_add theorem

(x y : V) : midpoint R 0 (x + y) = midpoint R x y

Full source

theorem midpoint_zero_add (x y : V) : midpoint R 0 (x + y) = midpoint R x y :=
  (midpoint_eq_midpoint_iff_vsub_eq_vsub R).2 <| by simp [sub_add_eq_sub_sub_swap]

Midpoint of Zero and Sum Equals Midpoint of Vectors

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vectors $x, y \in V$, the midpoint of the zero vector and $x + y$ is equal to the midpoint of $x$ and $y$, i.e., \[ \text{midpoint}_R(0, x + y) = \text{midpoint}_R(x, y). \]

midpoint_eq_smul_add theorem

(x y : V) : midpoint R x y = (⅟ 2 : R) • (x + y)

Full source

theorem midpoint_eq_smul_add (x y : V) : midpoint R x y = (⅟ 2 : R) • (x + y) := by
  rw [midpoint_eq_iff, pointReflection_apply, vsub_eq_sub, vadd_eq_add, sub_add_eq_add_sub, ←
    two_smul R, smul_smul, mul_invOf_self, one_smul, add_sub_cancel_left]

Midpoint Formula: $\text{midpoint}_R(x, y) = \frac{1}{2}(x + y)$

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vectors $x, y \in V$, the midpoint of $x$ and $y$ is given by the scalar multiplication of the inverse of $2$ with the sum of $x$ and $y$, i.e., \[ \text{midpoint}_R(x, y) = \frac{1}{2} (x + y). \]

midpoint_self_neg theorem

(x : V) : midpoint R x (-x) = 0

Full source

@[simp]
theorem midpoint_self_neg (x : V) : midpoint R x (-x) = 0 := by
  rw [midpoint_eq_smul_add, add_neg_cancel, smul_zero]

Midpoint of a Vector and its Negative is Zero

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vector $x \in V$, the midpoint of $x$ and $-x$ is the zero vector, i.e., \[ \text{midpoint}_R(x, -x) = 0. \]

midpoint_neg_self theorem

(x : V) : midpoint R (-x) x = 0

Full source

@[simp]
theorem midpoint_neg_self (x : V) : midpoint R (-x) x = 0 := by simpa using midpoint_self_neg R (-x)

Midpoint of Negative and Positive Vector is Zero

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vector $x \in V$, the midpoint of $-x$ and $x$ is the zero vector, i.e., \[ \text{midpoint}_R(-x, x) = 0. \]

midpoint_sub_add theorem

(x y : V) : midpoint R (x - y) (x + y) = x

Full source

@[simp]
theorem midpoint_sub_add (x y : V) : midpoint R (x - y) (x + y) = x := by
  rw [sub_eq_add_neg, ← vadd_eq_add, ← vadd_eq_add, ← midpoint_vadd_midpoint]; simp

Midpoint of $x - y$ and $x + y$ is $x$

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vectors $x, y \in V$, the midpoint of $x - y$ and $x + y$ is equal to $x$, i.e., \[ \text{midpoint}_R(x - y, x + y) = x. \]

midpoint_add_sub theorem

(x y : V) : midpoint R (x + y) (x - y) = x

Full source

@[simp]
theorem midpoint_add_sub (x y : V) : midpoint R (x + y) (x - y) = x := by
  rw [midpoint_comm]; simp

Midpoint of Sum and Difference is Original Vector: $\text{midpoint}(x + y, x - y) = x$

Informal description

Let $R$ be a ring with an invertible element $2$, and let $V$ be a module over $R$. For any vectors $x, y \in V$, the midpoint of $x + y$ and $x - y$ is equal to $x$, i.e., \[ \text{midpoint}_R(x + y, x - y) = x. \]

AddMonoidHom.ofMapMidpoint definition

(f : E → F) (h0 : f 0 = 0) (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) : E →+ F

Full source

/-- A map `f : E → F` sending zero to zero and midpoints to midpoints is an `AddMonoidHom`. -/
def ofMapMidpoint (f : E → F) (h0 : f 0 = 0)
    (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) : E →+ F where
  toFun := f
  map_zero' := h0
  map_add' x y :=
    calc
      f (x + y) = f 0 + f (x + y) := by rw [h0, zero_add]
      _ = midpoint R' (f 0) (f (x + y)) + midpoint R' (f 0) (f (x + y)) :=
        (midpoint_add_self _ _ _).symm
      _ = f (midpoint R x y) + f (midpoint R x y) := by rw [← hm, midpoint_zero_add]
      _ = f x + f y := by rw [hm, midpoint_add_self]

Additive Monoid Homomorphism from Midpoint-Preserving Map

Informal description

Given a map $f : E \to F$ between additive commutative groups that satisfies: 1. $f(0) = 0$ (preservation of zero) 2. $f$ preserves midpoints, i.e., $f(\text{midpoint}_R(x, y)) = \text{midpoint}_{R'}(f(x), f(y))$ for all $x, y \in E$ then $f$ is an additive monoid homomorphism from $E$ to $F$.

AddMonoidHom.coe_ofMapMidpoint theorem

 (f : E → F) (h0 : f 0 = 0) (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) :
  ⇑(ofMapMidpoint R R' f h0 hm) = f

Full source

@[simp]
theorem coe_ofMapMidpoint (f : E → F) (h0 : f 0 = 0)
    (hm : ∀ x y, f (midpoint R x y) = midpoint R' (f x) (f y)) :
    ⇑(ofMapMidpoint R R' f h0 hm) = f :=
  rfl

Underlying Function of Midpoint-Preserving Additive Monoid Homomorphism Equals Original Map

Informal description

Let $E$ and $F$ be additive commutative groups, and let $R$ and $R'$ be rings with invertible $2$. Given a map $f : E \to F$ satisfying: 1. $f(0) = 0$, and 2. $f$ preserves midpoints, i.e., $f(\text{midpoint}_R(x, y)) = \text{midpoint}_{R'}(f(x), f(y))$ for all $x, y \in E$, then the underlying function of the additive monoid homomorphism $\text{ofMapMidpoint}\, R\, R'\, f\, h0\, hm$ is equal to $f$.

Mathlib.LinearAlgebra.AffineSpace.Midpoint

Main definitions

Main theorems

Tags