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.
AddMonoidHom.ofMapMidpoint: construct an AddMonoidHom 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;
pointReflection_midpoint_left, pointReflection_midpoint_right: Equiv.pointReflection (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 #

midpoint, AddMonoidHom

def midpoint (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

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

Equations

midpoint R x y = ↑(AffineMap.lineMap x y) ⅟2

Instances For

source

@[simp]

theorem AffineMap.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] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] (f : P →ᵃ[R] P') (a : P) (b : P) :

↑f (midpoint R a b) = midpoint R (↑f a) (↑f b)

source

@[simp]

theorem AffineEquiv.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] [AddCommGroup V] [Module R V] [AddTorsor V P] [AddCommGroup V'] [Module R V'] [AddTorsor V' P'] (f : P ≃ᵃ[R] P') (a : P) (b : P) :

↑f (midpoint R a b) = midpoint R (↑f a) (↑f b)

source

theorem AffineEquiv.pointReflection_midpoint_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

↑(AffineEquiv.pointReflection R (midpoint R x y)) x = y

source

@[simp]

theorem Equiv.pointReflection_midpoint_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

↑(Equiv.pointReflection (midpoint R x y)) x = y

source

theorem midpoint_comm {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

midpoint R x y = midpoint R y x

source

theorem AffineEquiv.pointReflection_midpoint_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

↑(AffineEquiv.pointReflection R (midpoint R x y)) y = x

source

@[simp]

theorem Equiv.pointReflection_midpoint_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

↑(Equiv.pointReflection (midpoint R x y)) y = x

source

theorem midpoint_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) (p₃ : P) (p₄ : P) :

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

source

theorem midpoint_vadd_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (v : V) (v' : V) (p : P) (p' : P) :

midpoint R v v' +ᵥ midpoint R p p' = midpoint R (v +ᵥ p) (v' +ᵥ p')

source

theorem midpoint_eq_iff {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} {z : P} :

midpoint R x y = z ↔ ↑(AffineEquiv.pointReflection R z) x = y

source

@[simp]

theorem midpoint_pointReflection_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

midpoint R (↑(Equiv.pointReflection x) y) y = x

source

@[simp]

theorem midpoint_pointReflection_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) (y : P) :

midpoint R y (↑(Equiv.pointReflection x) y) = x

source

@[simp]

theorem midpoint_vsub_left {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) :

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

source

@[simp]

theorem midpoint_vsub_right {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) :

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

source

@[simp]

theorem left_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) :

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

source

@[simp]

theorem right_vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) :

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

source

theorem midpoint_vsub {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) (p : P) :

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

source

theorem vsub_midpoint {R : Type u_1} {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (p₁ : P) (p₂ : P) (p : P) :

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

source

@[simp]

theorem midpoint_sub_left {R : Type u_1} {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (v₁ : V) (v₂ : V) :

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

source

@[simp]

theorem midpoint_sub_right {R : Type u_1} {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (v₁ : V) (v₂ : V) :

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

source

@[simp]

theorem left_sub_midpoint {R : Type u_1} {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (v₁ : V) (v₂ : V) :

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

source

@[simp]

theorem right_sub_midpoint {R : Type u_1} {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (v₁ : V) (v₂ : V) :

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

source

@[simp]

theorem midpoint_eq_left_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} :

midpoint R x y = x ↔ x = y

source

@[simp]

theorem left_eq_midpoint_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} :

x = midpoint R x y ↔ x = y

source

@[simp]

theorem midpoint_eq_right_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} :

midpoint R x y = y ↔ x = y

source

@[simp]

theorem right_eq_midpoint_iff (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} :

y = midpoint R x y ↔ x = y

source

theorem midpoint_eq_midpoint_iff_vsub_eq_vsub (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {x' : P} {y : P} {y' : P} :

midpoint R x y = midpoint R x' y' ↔ x -ᵥ x' = y' -ᵥ y

source

theorem midpoint_eq_iff' (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] {x : P} {y : P} {z : P} :

midpoint R x y = z ↔ ↑(Equiv.pointReflection z) x = y

source

theorem midpoint_unique (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (R' : Type u_6) [Ring R'] [Invertible 2] [Module R' V] (x : P) (y : P) :

midpoint R x y = midpoint R' x y

midpoint does not depend on the ring R.

source

@[simp]

theorem midpoint_self (R : Type u_1) {V : Type u_2} {P : Type u_4} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] [AddTorsor V P] (x : P) :

midpoint R x x = x

source

@[simp]

theorem midpoint_add_self (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) (y : V) :

midpoint R x y + midpoint R x y = x + y

source

theorem midpoint_zero_add (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) (y : V) :

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

source

theorem midpoint_eq_smul_add (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) (y : V) :

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

source

@[simp]

theorem midpoint_self_neg (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) :

midpoint R x (-x) = 0

source

@[simp]

theorem midpoint_neg_self (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) :

midpoint R (-x) x = 0

source

@[simp]

theorem midpoint_sub_add (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) (y : V) :

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

source

@[simp]

theorem midpoint_add_sub (R : Type u_1) {V : Type u_2} [Ring R] [Invertible 2] [AddCommGroup V] [Module R V] (x : V) (y : V) :

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

source

def AddMonoidHom.ofMapMidpoint (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [Ring R] [Invertible 2] [AddCommGroup E] [Module R E] [Ring R'] [Invertible 2] [AddCommGroup F] [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 AddMonoidHom.

Equations

AddMonoidHom.ofMapMidpoint R R' f h0 hm = { toZeroHom := { toFun := f, map_zero' := h0 }, map_add' := (_ : ∀ (x y : E), f (x + y) = f x + f y) }

Instances For

source

@[simp]

theorem AddMonoidHom.coe_ofMapMidpoint (R : Type u_1) (R' : Type u_2) {E : Type u_3} {F : Type u_4} [Ring R] [Invertible 2] [AddCommGroup E] [Module R E] [Ring R'] [Invertible 2] [AddCommGroup F] [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)) :

↑(AddMonoidHom.ofMapMidpoint R R' f h0 hm) = f