Midpoint of a segment
Main definitions
midpoint R x y: midpoint of the segment[x, y]. We define it forxandyin a module over a ringRwith invertible2.add_monoid_hom.of_map_midpoint: construct anadd_monoid_homgiven a mapfsuch thatfsends zero to zero and midpoints to midpoints.
Main theorems
midpoint_eq_iff:zis the midpoint of[x, y]if and only ifx + y = z + z,midpoint_unique:midpoint R x ydoes not depend onR;midpoint x yis linear both inxandy;point_reflection_midpoint_left,point_reflection_midpoint_right:equiv.point_reflection (midpoint R x y)swapsxandy.
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].
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} :
@[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) :
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 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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
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) :
A map f : E → F sending zero to zero and midpoints to midpoints is an add_monoid_hom.
@[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)) :
⇑(add_monoid_hom.of_map_midpoint R R' f h0 hm) = f
@[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) :
⇑(equiv.point_reflection (midpoint R x y)) x = y
@[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) :
⇑(equiv.point_reflection (midpoint R x y)) y = x