mathlib documentation

algebra.midpoint

Midpoint of a segment

Main definitions

Main theorems

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

Tags

midpoint, add_monoid_hom

def midpoint (R : Type u_1) {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] :
E → E → E

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

Equations
theorem midpoint_eq_iff (R : Type u_1) {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] {x y z : E} :
midpoint R x y = z x + y = z + z

@[simp]
theorem midpoint_add_self (R : Type u_1) {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y : E) :
midpoint R x y + midpoint R x y = x + y

theorem midpoint_unique (R : Type u_1) {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (R' : Type u_3) [semiring R'] [invertible 2] [semimodule R' E] (x y : E) :
midpoint R x y = midpoint R' x y

midpoint does not depend on the ring R.

@[simp]
theorem midpoint_self (R : Type u_1) {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x : E) :
midpoint R x x = x

theorem midpoint_def {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y : E) :
midpoint R x y = 2 (x + y)

theorem midpoint_comm {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y : E) :
midpoint R x y = midpoint R y x

theorem midpoint_zero_add {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y : E) :
midpoint R 0 (x + y) = midpoint R x y

theorem midpoint_add_add {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y x' y' : E) :
midpoint R (x + x') (y + y') = midpoint R x y + midpoint R x' y'

theorem midpoint_add_right {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y z : E) :
midpoint R (x + z) (y + z) = midpoint R x y + z

theorem midpoint_add_left {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (x y z : E) :
midpoint R (x + y) (x + z) = x + midpoint R y z

theorem midpoint_smul_smul {R : Type u_1} {E : Type u_2} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] (c : R) (x y : E) :
midpoint R (c x) (c y) = c midpoint R x y

theorem midpoint_neg_neg (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y : E) :
midpoint R (-x) (-y) = -midpoint R x y

theorem midpoint_sub_sub (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y x' y' : E) :
midpoint R (x - x') (y - y') = midpoint R x y - midpoint R x' y'

theorem midpoint_sub_right (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y z : E) :
midpoint R (x - z) (y - z) = midpoint R x y - z

theorem midpoint_sub_left (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y z : E) :
midpoint R (x - y) (x - z) = x - midpoint R y z

def add_monoid_hom.of_map_midpoint (R : Type u_1) {E : Type u_2} (R' : Type u_3) {F : Type u_4} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] [semiring R'] [invertible 2] [add_comm_monoid F] [semimodule R' F] (f : E → F) :
f 0 = 0(∀ (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) {E : Type u_2} (R' : Type u_3) {F : Type u_4} [semiring R] [invertible 2] [add_comm_monoid E] [semimodule R E] [semiring R'] [invertible 2] [add_comm_monoid F] [semimodule R' F] (f : E → F) (h0 : f 0 = 0) (hm : ∀ (x y : E), f (midpoint R x y) = midpoint R' (f x) (f y)) :

@[simp]
theorem equiv.point_reflection_midpoint_left (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y : E) :

@[simp]
theorem equiv.point_reflection_midpoint_right (R : Type u_1) {E : Type u_2} [ring R] [invertible 2] [add_comm_group E] [module R E] (x y : E) :