# mathlibdocumentation

linear_algebra.affine_space.midpoint

# Midpoint of a segment #

## Main definitions #

• midpoint R x y: midpoint of the segment [x, y]. We define it for x and y in a module over a ring R with invertible 2.
• add_monoid_hom.of_map_midpoint: construct an add_monoid_hom given a map f such that f sends zero to zero and midpoints to midpoints.

## Main theorems #

• midpoint_eq_iff: z is the midpoint of [x, y] if and only if x + y = z + z,
• midpoint_unique: midpoint R x y does not depend on R;
• midpoint x y is linear both in x and y;
• point_reflection_midpoint_left, point_reflection_midpoint_right: equiv.point_reflection (midpoint R x y) swaps x and y.

We do not mark most lemmas as @[simp] because it is hard to tell which side is simpler.

## Tags #

def midpoint (R : Type u_1) {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (x y : P) :
P

midpoint x y is the midpoint of the segment [x, y].

Equations
@[simp]
theorem affine_map.map_midpoint {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ring R] [invertible 2] [ V] [ P] [add_comm_group V'] [ V'] [ P'] (f : P →ᵃ[R] P') (a b : P) :
f (midpoint R a b) = (f a) (f b)
@[simp]
theorem affine_equiv.map_midpoint {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [ring R] [invertible 2] [ V] [ P] [add_comm_group V'] [ V'] [ P'] (f : P ≃ᵃ[R] P') (a b : P) :
f (midpoint R a b) = (f a) (f b)
@[simp]
theorem affine_equiv.point_reflection_midpoint_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (x y : P) :
(midpoint R x y)) x = y
theorem midpoint_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (x y : P) :
x y = y x
@[simp]
theorem affine_equiv.point_reflection_midpoint_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (x y : P) :
(midpoint R x y)) y = x
theorem midpoint_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (p₁ p₂ p₃ p₄ : P) :
p₁ p₂ -ᵥ p₃ p₄ = (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)
theorem midpoint_vadd_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (v v' : V) (p p' : P) :
v v' +ᵥ p p' = (v +ᵥ p) (v' +ᵥ p')
theorem midpoint_eq_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] {x y z : P} :
x y = z = y
@[simp]
theorem midpoint_vsub_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (p₁ p₂ : P) :
p₁ p₂ -ᵥ p₁ = 2 (p₂ -ᵥ p₁)
@[simp]
theorem midpoint_vsub_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (p₁ p₂ : P) :
p₁ p₂ -ᵥ p₂ = 2 (p₁ -ᵥ p₂)
@[simp]
theorem left_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (p₁ p₂ : P) :
p₁ -ᵥ p₁ p₂ = 2 (p₁ -ᵥ p₂)
@[simp]
theorem right_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (p₁ p₂ : P) :
p₂ -ᵥ p₁ p₂ = 2 (p₂ -ᵥ p₁)
@[simp]
theorem midpoint_sub_left {R : Type u_1} {V : Type u_2} [ring R] [invertible 2] [ V] (v₁ v₂ : V) :
v₁ v₂ - v₁ = 2 (v₂ - v₁)
@[simp]
theorem midpoint_sub_right {R : Type u_1} {V : Type u_2} [ring R] [invertible 2] [ V] (v₁ v₂ : V) :
v₁ v₂ - v₂ = 2 (v₁ - v₂)
@[simp]
theorem left_sub_midpoint {R : Type u_1} {V : Type u_2} [ring R] [invertible 2] [ V] (v₁ v₂ : V) :
v₁ - v₁ v₂ = 2 (v₁ - v₂)
@[simp]
theorem right_sub_midpoint {R : Type u_1} {V : Type u_2} [ring R] [invertible 2] [ V] (v₁ v₂ : V) :
v₂ - v₁ v₂ = 2 (v₂ - v₁)
theorem midpoint_eq_midpoint_iff_vsub_eq_vsub (R : Type u_1) {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] {x x' y y' : P} :
x y = x' y' x -ᵥ x' = y' -ᵥ y
theorem midpoint_eq_iff' (R : Type u_1) {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] {x y z : P} :
x y = z = y
theorem midpoint_unique (R : Type u_1) {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (R' : Type u_3) [ring R'] [invertible 2] [module R' V] (x y : P) :
x y = midpoint R' x y

midpoint does not depend on the ring R.

@[simp]
theorem midpoint_self (R : Type u_1) {V : Type u_2} {P : Type u_4} [ring R] [invertible 2] [ V] [ P] (x : P) :
x x = x
@[simp]
theorem midpoint_add_self (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x y : V) :
x y + x y = x + y
theorem midpoint_zero_add (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x y : V) :
0 (x + y) = x y
theorem midpoint_eq_smul_add (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x y : V) :
x y = 2 (x + y)
@[simp]
theorem midpoint_self_neg (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x : V) :
x (-x) = 0
@[simp]
theorem midpoint_neg_self (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x : V) :
(-x) x = 0
@[simp]
theorem midpoint_sub_add (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x y : V) :
(x - y) (x + y) = x
@[simp]
theorem midpoint_add_sub (R : Type u_1) {V : Type u_2} [ring R] [invertible 2] [ V] (x y : V) :
(x + y) (x - y) = x
theorem line_map_inv_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [char_zero R] [ V] [ P] (a b : P) :
b) 2⁻¹ = a b
theorem line_map_one_half {R : Type u_1} {V : Type u_2} {P : Type u_3} [char_zero R] [ V] [ P] (a b : P) :
b) (1 / 2) = a b
theorem homothety_inv_of_two {R : Type u_1} {V : Type u_2} {P : Type u_3} [comm_ring R] [invertible 2] [ V] [ P] (a b : P) :
( 2)) b = a b
theorem homothety_inv_two {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [ V] [ P] (a b : P) :
b = a b
theorem homothety_one_half {k : Type u_1} {V : Type u_2} {P : Type u_3} [field k] [char_zero k] [ V] [ P] (a b : P) :
(1 / 2)) b = a b
@[simp]
theorem pi_midpoint_apply {k : Type u_1} {ι : Type u_2} {V : ι → Type u_3} {P : ι → Type u_4} [field k] [invertible 2] [Π (i : ι), add_comm_group (V i)] [Π (i : ι), (V i)] [Π (i : ι), add_torsor (V i) (P i)] (f g : Π (i : ι), P i) (i : ι) :
f g i = (f i) (g i)
def add_monoid_hom.of_map_midpoint (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [ring R] [invertible 2] [ E] [ring R'] [invertible 2] [module R' F] (f : E → F) (h0 : f 0 = 0) (hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)) :
E →+ F

A map f : E → F sending zero to zero and midpoints to midpoints is an add_monoid_hom.

Equations
@[simp]
theorem add_monoid_hom.coe_of_map_midpoint (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [ring R] [invertible 2] [ E] [ring R'] [invertible 2] [module R' F] (f : E → F) (h0 : f 0 = 0) (hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)) :
h0 hm) = f