geometry.euclidean.basic

noncomputable def inner_product_geometry.angle {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

The undirected angle between two vectors. If either vector is 0, this is π/2. See orientation.oangle for the corresponding oriented angle definition.

Equations

inner_product_geometry.angle x y = real.arccos (has_inner.inner x y / (∥x∥ * ∥y∥))

source

theorem inner_product_geometry.continuous_at_angle {V : Type u_1} [inner_product_space ℝ V] {x : V × V} (hx1 : x.fst ≠ 0) (hx2 : x.snd ≠ 0) :

continuous_at (λ (y : V × V), inner_product_geometry.angle y.fst y.snd) x

source

theorem inner_product_geometry.angle_smul_smul {V : Type u_1} [inner_product_space ℝ V] {c : ℝ} (hc : c ≠ 0) (x y : V) :

inner_product_geometry.angle (c • x) (c • y) = inner_product_geometry.angle x y

source

@[simp]

theorem linear_isometry.angle_map {E : Type u_1} {F : Type u_2} [inner_product_space ℝ E] [inner_product_space ℝ F] (f : E →ₗᵢ[ℝ ] F) (u v : E) :

inner_product_geometry.angle (⇑f u) (⇑f v) = inner_product_geometry.angle u v

source

theorem inner_product_geometry.is_conformal_map.preserves_angle {E : Type u_1} {F : Type u_2} [inner_product_space ℝ E] [inner_product_space ℝ F] {f' : E →L[ℝ ] F} (h : is_conformal_map f') (u v : E) :

inner_product_geometry.angle (⇑f' u) (⇑f' v) = inner_product_geometry.angle u v

source

theorem inner_product_geometry.conformal_at.preserves_angle {E : Type u_1} {F : Type u_2} [inner_product_space ℝ E] [inner_product_space ℝ F] {f : E → F} {x : E} {f' : E →L[ℝ ] F} (h : has_fderiv_at f f' x) (H : conformal_at f x) (u v : E) :

inner_product_geometry.angle (⇑f' u) (⇑f' v) = inner_product_geometry.angle u v

If a real differentiable map f is conformal at a point x, then it preserves the angles at that point.

source

theorem inner_product_geometry.cos_angle {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

real.cos (inner_product_geometry.angle x y) = has_inner.inner x y / (∥x∥ * ∥y∥)

The cosine of the angle between two vectors.

source

theorem inner_product_geometry.angle_comm {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

inner_product_geometry.angle x y = inner_product_geometry.angle y x

The angle between two vectors does not depend on their order.

source

@[simp]

theorem inner_product_geometry.angle_neg_neg {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

inner_product_geometry.angle (-x) (-y) = inner_product_geometry.angle x y

The angle between the negation of two vectors.

source

theorem inner_product_geometry.angle_nonneg {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

0 ≤ inner_product_geometry.angle x y

The angle between two vectors is nonnegative.

source

theorem inner_product_geometry.angle_le_pi {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

inner_product_geometry.angle x y ≤ real.pi

The angle between two vectors is at most π.

source

theorem inner_product_geometry.angle_neg_right {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

inner_product_geometry.angle x (-y) = real.pi - inner_product_geometry.angle x y

The angle between a vector and the negation of another vector.

source

theorem inner_product_geometry.angle_neg_left {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

inner_product_geometry.angle (-x) y = real.pi - inner_product_geometry.angle x y

The angle between the negation of a vector and another vector.

source

@[simp]

theorem inner_product_geometry.angle_zero_left {V : Type u_1} [inner_product_space ℝ V] (x : V) :

inner_product_geometry.angle 0 x = real.pi / 2

The angle between the zero vector and a vector.

source

@[simp]

theorem inner_product_geometry.angle_zero_right {V : Type u_1} [inner_product_space ℝ V] (x : V) :

inner_product_geometry.angle x 0 = real.pi / 2

The angle between a vector and the zero vector.

source

@[simp]

theorem inner_product_geometry.angle_self {V : Type u_1} [inner_product_space ℝ V] {x : V} (hx : x ≠ 0) :

inner_product_geometry.angle x x = 0

The angle between a nonzero vector and itself.

source

@[simp]

theorem inner_product_geometry.angle_self_neg_of_nonzero {V : Type u_1} [inner_product_space ℝ V] {x : V} (hx : x ≠ 0) :

inner_product_geometry.angle x (-x) = real.pi

The angle between a nonzero vector and its negation.

source

@[simp]

theorem inner_product_geometry.angle_neg_self_of_nonzero {V : Type u_1} [inner_product_space ℝ V] {x : V} (hx : x ≠ 0) :

inner_product_geometry.angle (-x) x = real.pi

The angle between the negation of a nonzero vector and that vector.

source

@[simp]

theorem inner_product_geometry.angle_smul_right_of_pos {V : Type u_1} [inner_product_space ℝ V] (x y : V) {r : ℝ} (hr : 0 < r) :

inner_product_geometry.angle x (r • y) = inner_product_geometry.angle x y

The angle between a vector and a positive multiple of a vector.

source

@[simp]

theorem inner_product_geometry.angle_smul_left_of_pos {V : Type u_1} [inner_product_space ℝ V] (x y : V) {r : ℝ} (hr : 0 < r) :

inner_product_geometry.angle (r • x) y = inner_product_geometry.angle x y

The angle between a positive multiple of a vector and a vector.

source

@[simp]

theorem inner_product_geometry.angle_smul_right_of_neg {V : Type u_1} [inner_product_space ℝ V] (x y : V) {r : ℝ} (hr : r < 0) :

inner_product_geometry.angle x (r • y) = inner_product_geometry.angle x (-y)

The angle between a vector and a negative multiple of a vector.

source

@[simp]

theorem inner_product_geometry.angle_smul_left_of_neg {V : Type u_1} [inner_product_space ℝ V] (x y : V) {r : ℝ} (hr : r < 0) :

inner_product_geometry.angle (r • x) y = inner_product_geometry.angle (-x) y

The angle between a negative multiple of a vector and a vector.

source

theorem inner_product_geometry.cos_angle_mul_norm_mul_norm {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

real.cos (inner_product_geometry.angle x y) * (∥x∥ * ∥y∥) = has_inner.inner x y

The cosine of the angle between two vectors, multiplied by the product of their norms.

source

theorem inner_product_geometry.sin_angle_mul_norm_mul_norm {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

real.sin (inner_product_geometry.angle x y) * (∥x∥ * ∥y∥) = real.sqrt (has_inner.inner x x * has_inner.inner y y - has_inner.inner x y * has_inner.inner x y)

The sine of the angle between two vectors, multiplied by the product of their norms.

source

theorem inner_product_geometry.angle_eq_zero_iff {V : Type u_1} [inner_product_space ℝ V] {x y : V} :

inner_product_geometry.angle x y = 0 ↔ x ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • x

The angle between two vectors is zero if and only if they are nonzero and one is a positive multiple of the other.

source

theorem inner_product_geometry.angle_eq_pi_iff {V : Type u_1} [inner_product_space ℝ V] {x y : V} :

inner_product_geometry.angle x y = real.pi ↔ x ≠ 0 ∧ ∃ (r : ℝ), r < 0 ∧ y = r • x

The angle between two vectors is π if and only if they are nonzero and one is a negative multiple of the other.

source

theorem inner_product_geometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} [inner_product_space ℝ V] {x y : V} (z : V) (h : inner_product_geometry.angle x y = real.pi) :

inner_product_geometry.angle x z + inner_product_geometry.angle y z = real.pi

If the angle between two vectors is π, the angles between those vectors and a third vector add to π.

source

theorem inner_product_geometry.inner_eq_zero_iff_angle_eq_pi_div_two {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

has_inner.inner x y = 0 ↔ inner_product_geometry.angle x y = real.pi / 2

Two vectors have inner product 0 if and only if the angle between them is π/2.

source

theorem inner_product_geometry.inner_eq_neg_mul_norm_of_angle_eq_pi {V : Type u_1} [inner_product_space ℝ V] {x y : V} (h : inner_product_geometry.angle x y = real.pi) :

has_inner.inner x y = -(∥x∥ * ∥y∥)

If the angle between two vectors is π, the inner product equals the negative product of the norms.

source

theorem inner_product_geometry.inner_eq_mul_norm_of_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (h : inner_product_geometry.angle x y = 0) :

has_inner.inner x y = ∥x∥ * ∥y∥

If the angle between two vectors is 0, the inner product equals the product of the norms.

source

theorem inner_product_geometry.inner_eq_neg_mul_norm_iff_angle_eq_pi {V : Type u_1} [inner_product_space ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :

has_inner.inner x y = -(∥x∥ * ∥y∥) ↔ inner_product_geometry.angle x y = real.pi

The inner product of two non-zero vectors equals the negative product of their norms if and only if the angle between the two vectors is π.

source

theorem inner_product_geometry.inner_eq_mul_norm_iff_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :

has_inner.inner x y = ∥x∥ * ∥y∥ ↔ inner_product_geometry.angle x y = 0

The inner product of two non-zero vectors equals the product of their norms if and only if the angle between the two vectors is 0.

source

theorem inner_product_geometry.norm_sub_eq_add_norm_of_angle_eq_pi {V : Type u_1} [inner_product_space ℝ V] {x y : V} (h : inner_product_geometry.angle x y = real.pi) :

∥x - y∥ = ∥x∥ + ∥y∥

If the angle between two vectors is π, the norm of their difference equals the sum of their norms.

source

theorem inner_product_geometry.norm_add_eq_add_norm_of_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (h : inner_product_geometry.angle x y = 0) :

∥x + y∥ = ∥x∥ + ∥y∥

If the angle between two vectors is 0, the norm of their sum equals the sum of their norms.

source

theorem inner_product_geometry.norm_sub_eq_abs_sub_norm_of_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (h : inner_product_geometry.angle x y = 0) :

∥x - y∥ = |∥x∥ - ∥y∥|

If the angle between two vectors is 0, the norm of their difference equals the absolute value of the difference of their norms.

source

theorem inner_product_geometry.norm_sub_eq_add_norm_iff_angle_eq_pi {V : Type u_1} [inner_product_space ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :

∥x - y∥ = ∥x∥ + ∥y∥ ↔ inner_product_geometry.angle x y = real.pi

The norm of the difference of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is π.

source

theorem inner_product_geometry.norm_add_eq_add_norm_iff_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :

∥x + y∥ = ∥x∥ + ∥y∥ ↔ inner_product_geometry.angle x y = 0

The norm of the sum of two non-zero vectors equals the sum of their norms if and only the angle between the two vectors is 0.

source

theorem inner_product_geometry.norm_sub_eq_abs_sub_norm_iff_angle_eq_zero {V : Type u_1} [inner_product_space ℝ V] {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :

∥x - y∥ = |∥x∥ - ∥y∥| ↔ inner_product_geometry.angle x y = 0

The norm of the difference of two non-zero vectors equals the absolute value of the difference of their norms if and only the angle between the two vectors is 0.

source

theorem inner_product_geometry.norm_add_eq_norm_sub_iff_angle_eq_pi_div_two {V : Type u_1} [inner_product_space ℝ V] (x y : V) :

∥x + y∥ = ∥x - y∥ ↔ inner_product_geometry.angle x y = real.pi / 2

The norm of the sum of two vectors equals the norm of their difference if and only if the angle between them is π/2.

source

noncomputable def euclidean_geometry.angle {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :

ℝ

The undirected angle at p2 between the line segments to p1 and p3. If either of those points equals p2, this is π/2. Use open_locale euclidean_geometry to access the ∠ p1 p2 p3 notation.

Equations

euclidean_geometry.angle p1 p2 p3 = inner_product_geometry.angle (p1 -ᵥ p2) (p3 -ᵥ p2)

source

theorem euclidean_geometry.continuous_at_angle {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {x : P × P × P} (hx12 : x.fst ≠ x.snd.fst) (hx32 : x.snd.snd ≠ x.snd.fst) :

continuous_at (λ (y : P × P × P), euclidean_geometry.angle y.fst y.snd.fst y.snd.snd) x

source

theorem euclidean_geometry.angle_comm {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :

euclidean_geometry.angle p1 p2 p3 = euclidean_geometry.angle p3 p2 p1

The angle at a point does not depend on the order of the other two points.

source

theorem euclidean_geometry.angle_nonneg {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :

0 ≤ euclidean_geometry.angle p1 p2 p3

The angle at a point is nonnegative.

source

theorem euclidean_geometry.angle_le_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 p3 : P) :

euclidean_geometry.angle p1 p2 p3 ≤ real.pi

The angle at a point is at most π.

source

theorem euclidean_geometry.angle_eq_left {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 : P) :

euclidean_geometry.angle p1 p1 p2 = real.pi / 2

The angle ∠AAB at a point.

source

theorem euclidean_geometry.angle_eq_right {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 : P) :

euclidean_geometry.angle p1 p2 p2 = real.pi / 2

The angle ∠ABB at a point.

source

theorem euclidean_geometry.angle_eq_of_ne {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 : P} (h : p1 ≠ p2) :

euclidean_geometry.angle p1 p2 p1 = 0

The angle ∠ABA at a point.

source

theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_left {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = real.pi) :

euclidean_geometry.angle p2 p1 p3 = 0

If the angle ∠ABC at a point is π, the angle ∠BAC is 0.

source

theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_right {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = real.pi) :

euclidean_geometry.angle p2 p3 p1 = 0

If the angle ∠ABC at a point is π, the angle ∠BCA is 0.

source

theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 : P) {p2 p3 p4 : P} (h : euclidean_geometry.angle p2 p3 p4 = real.pi) :

euclidean_geometry.angle p1 p2 p3 = euclidean_geometry.angle p1 p2 p4

If ∠BCD = π, then ∠ABC = ∠ABD.

source

theorem euclidean_geometry.angle_add_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 : P) {p2 p3 p4 : P} (h : euclidean_geometry.angle p2 p3 p4 = real.pi) :

euclidean_geometry.angle p1 p3 p2 + euclidean_geometry.angle p1 p3 p4 = real.pi

If ∠BCD = π, then ∠ACB + ∠ACD = π.

source

theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 p4 p5 : P} (hapc : euclidean_geometry.angle p1 p5 p3 = real.pi) (hbpd : euclidean_geometry.angle p2 p5 p4 = real.pi) :

euclidean_geometry.angle p1 p5 p2 = euclidean_geometry.angle p3 p5 p4

Vertical Angles Theorem: angles opposite each other, formed by two intersecting straight lines, are equal.

source

theorem euclidean_geometry.left_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = real.pi) :

has_dist.dist p1 p2 ≠ 0

If ∠ABC = π then dist A B ≠ 0.

source

theorem euclidean_geometry.right_dist_ne_zero_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = real.pi) :

has_dist.dist p3 p2 ≠ 0

If ∠ABC = π then dist C B ≠ 0.

source

theorem euclidean_geometry.dist_eq_add_dist_of_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = real.pi) :

has_dist.dist p1 p3 = has_dist.dist p1 p2 + has_dist.dist p3 p2

If ∠ABC = π, then (dist A C) = (dist A B) + (dist B C).

source

theorem euclidean_geometry.dist_eq_add_dist_iff_angle_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :

has_dist.dist p1 p3 = has_dist.dist p1 p2 + has_dist.dist p3 p2 ↔ euclidean_geometry.angle p1 p2 p3 = real.pi

If A ≠ B and C ≠ B then ∠ABC = π if and only if (dist A C) = (dist A B) + (dist B C).

source

theorem euclidean_geometry.dist_eq_abs_sub_dist_of_angle_eq_zero {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : euclidean_geometry.angle p1 p2 p3 = 0) :

has_dist.dist p1 p3 = |has_dist.dist p1 p2 - has_dist.dist p3 p2|

If ∠ABC = 0, then (dist A C) = abs ((dist A B) - (dist B C)).

source

theorem euclidean_geometry.dist_eq_abs_sub_dist_iff_angle_eq_zero {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (hp1p2 : p1 ≠ p2) (hp3p2 : p3 ≠ p2) :

has_dist.dist p1 p3 = |has_dist.dist p1 p2 - has_dist.dist p3 p2| ↔ euclidean_geometry.angle p1 p2 p3 = 0

If A ≠ B and C ≠ B then ∠ABC = 0 if and only if (dist A C) = abs ((dist A B) - (dist B C)).

source

theorem euclidean_geometry.dist_left_midpoint_eq_dist_right_midpoint {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 : P) :

has_dist.dist p1 (midpoint ℝ p1 p2) = has_dist.dist p2 (midpoint ℝ p1 p2)

The midpoint of the segment AB is the same distance from A as it is from B.

source

theorem euclidean_geometry.angle_midpoint_eq_pi {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p1 p2 : P) (hp1p2 : p1 ≠ p2) :

euclidean_geometry.angle p1 (midpoint ℝ p1 p2) p2 = real.pi

If M is the midpoint of the segment AB, then ∠AMB = π.

source

theorem euclidean_geometry.angle_left_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : has_dist.dist p3 p1 = has_dist.dist p3 p2) :

euclidean_geometry.angle p3 (midpoint ℝ p1 p2) p1 = real.pi / 2

If M is the midpoint of the segment AB and C is the same distance from A as it is from B then ∠CMA = π / 2.

source

theorem euclidean_geometry.angle_right_midpoint_eq_pi_div_two_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {p1 p2 p3 : P} (h : has_dist.dist p3 p1 = has_dist.dist p3 p2) :

euclidean_geometry.angle p3 (midpoint ℝ p1 p2) p2 = real.pi / 2

If M is the midpoint of the segment AB and C is the same distance from A as it is from B then ∠CMB = π / 2.

source

theorem euclidean_geometry.inner_weighted_vsub {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {ι₁ : Type u_3} {s₁ : finset ι₁} {w₁ : ι₁ → ℝ} (p₁ : ι₁ → P) (h₁ : s₁.sum (λ (i : ι₁), w₁ i) = 0) {ι₂ : Type u_4} {s₂ : finset ι₂} {w₂ : ι₂ → ℝ} (p₂ : ι₂ → P) (h₂ : s₂.sum (λ (i : ι₂), w₂ i) = 0) :

has_inner.inner (⇑(s₁.weighted_vsub p₁) w₁) (⇑(s₂.weighted_vsub p₂) w₂) = -s₁.sum (λ (i₁ : ι₁), s₂.sum (λ (i₂ : ι₂), w₁ i₁ * w₂ i₂ * (has_dist.dist (p₁ i₁) (p₂ i₂) * has_dist.dist (p₁ i₁) (p₂ i₂)))) / 2

The inner product of two vectors given with weighted_vsub, in terms of the pairwise distances.

source

theorem euclidean_geometry.dist_affine_combination {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {ι : Type u_3} {s : finset ι} {w₁ w₂ : ι → ℝ} (p : ι → P) (h₁ : s.sum (λ (i : ι), w₁ i) = 1) (h₂ : s.sum (λ (i : ι), w₂ i) = 1) :

has_dist.dist (⇑(s.affine_combination p) w₁) (⇑(s.affine_combination p) w₂) * has_dist.dist (⇑(s.affine_combination p) w₁) (⇑(s.affine_combination p) w₂) = -s.sum (λ (i₁ : ι), s.sum (λ (i₂ : ι), (w₁ - w₂) i₁ * (w₁ - w₂) i₂ * (has_dist.dist (p i₁) (p i₂) * has_dist.dist (p i₁) (p i₂)))) / 2

The distance between two points given with affine_combination, in terms of the pairwise distances between the points in that combination.

source

theorem euclidean_geometry.inner_vsub_vsub_of_dist_eq_of_dist_eq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {c₁ c₂ p₁ p₂ : P} (hc₁ : has_dist.dist p₁ c₁ = has_dist.dist p₂ c₁) (hc₂ : has_dist.dist p₁ c₂ = has_dist.dist p₂ c₂) :

has_inner.inner (c₂ -ᵥ c₁) (p₂ -ᵥ p₁) = 0

Suppose that c₁ is equidistant from p₁ and p₂, and the same applies to c₂. Then the vector between c₁ and c₂ is orthogonal to that between p₁ and p₂. (In two dimensions, this says that the diagonals of a kite are orthogonal.)

source

theorem euclidean_geometry.dist_smul_vadd_sq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (r : ℝ) (v : V) (p₁ p₂ : P) :

has_dist.dist (r • v +ᵥ p₁) p₂ * has_dist.dist (r • v +ᵥ p₁) p₂ = has_inner.inner v v * r * r + 2 * has_inner.inner v (p₁ -ᵥ p₂) * r + has_inner.inner (p₁ -ᵥ p₂) (p₁ -ᵥ p₂)

The squared distance between points on a line (expressed as a multiple of a fixed vector added to a point) and another point, expressed as a quadratic.

source

theorem euclidean_geometry.dist_smul_vadd_eq_dist {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {v : V} (p₁ p₂ : P) (hv : v ≠ 0) (r : ℝ) :

has_dist.dist (r • v +ᵥ p₁) p₂ = has_dist.dist p₁ p₂ ↔ r = 0 ∨ r = (-2) * has_inner.inner v (p₁ -ᵥ p₂) / has_inner.inner v v

The condition for two points on a line to be equidistant from another point.

source

theorem euclidean_geometry.eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [finite_dimensional ℝ ↥(s.direction)] (hd : finite_dimensional.finrank ℝ ↥(s.direction) = 2) {c₁ c₂ p₁ p₂ p : P} (hc₁s : c₁ ∈ s) (hc₂s : c₂ ∈ s) (hp₁s : p₁ ∈ s) (hp₂s : p₂ ∈ s) (hps : p ∈ s) {r₁ r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : has_dist.dist p₁ c₁ = r₁) (hp₂c₁ : has_dist.dist p₂ c₁ = r₁) (hpc₁ : has_dist.dist p c₁ = r₁) (hp₁c₂ : has_dist.dist p₁ c₂ = r₂) (hp₂c₂ : has_dist.dist p₂ c₂ = r₂) (hpc₂ : has_dist.dist p c₂ = r₂) :

p = p₁ ∨ p = p₂

Distances r₁ r₂ of p from two different points c₁ c₂ determine at most two points p₁ p₂ in a two-dimensional subspace containing those points (two circles intersect in at most two points).

source

theorem euclidean_geometry.eq_of_dist_eq_of_dist_eq_of_finrank_eq_two {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] [finite_dimensional ℝ V] (hd : finite_dimensional.finrank ℝ V = 2) {c₁ c₂ p₁ p₂ p : P} {r₁ r₂ : ℝ} (hc : c₁ ≠ c₂) (hp : p₁ ≠ p₂) (hp₁c₁ : has_dist.dist p₁ c₁ = r₁) (hp₂c₁ : has_dist.dist p₂ c₁ = r₁) (hpc₁ : has_dist.dist p c₁ = r₁) (hp₁c₂ : has_dist.dist p₁ c₂ = r₂) (hp₂c₂ : has_dist.dist p₂ c₂ = r₂) (hpc₂ : has_dist.dist p c₂ = r₂) :

p = p₁ ∨ p = p₂

Distances r₁ r₂ of p from two different points c₁ c₂ determine at most two points p₁ p₂ in two-dimensional space (two circles intersect in at most two points).

source

noncomputable def euclidean_geometry.orthogonal_projection_fn {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

P

The orthogonal projection of a point onto a nonempty affine subspace, whose direction is complete, as an unbundled function. This definition is only intended for use in setting up the bundled version orthogonal_projection and should not be used once that is defined.

Equations

euclidean_geometry.orthogonal_projection_fn s p = classical.some _

source

theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection_fn {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

↑s ∩ ↑(affine_subspace.mk' p (s.direction)ᗮ) = {euclidean_geometry.orthogonal_projection_fn s p}

The intersection of the subspace and the orthogonal subspace through the given point is the orthogonal_projection_fn of that point onto the subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

source

theorem euclidean_geometry.orthogonal_projection_fn_mem {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

euclidean_geometry.orthogonal_projection_fn s p ∈ s

The orthogonal_projection_fn lies in the given subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

source

theorem euclidean_geometry.orthogonal_projection_fn_mem_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

euclidean_geometry.orthogonal_projection_fn s p ∈ affine_subspace.mk' p (s.direction)ᗮ

The orthogonal_projection_fn lies in the orthogonal subspace. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

source

theorem euclidean_geometry.orthogonal_projection_fn_vsub_mem_direction_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

euclidean_geometry.orthogonal_projection_fn s p -ᵥ p ∈ (s.direction)ᗮ

Subtracting p from its orthogonal_projection_fn produces a result in the orthogonal direction. This lemma is only intended for use in setting up the bundled version and should not be used once that is defined.

source

noncomputable def euclidean_geometry.orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] :

P →ᵃ[ℝ ] ↥s

The orthogonal projection of a point onto a nonempty affine subspace, whose direction is complete. The corresponding linear map (mapping a vector to the difference between the projections of two points whose difference is that vector) is the orthogonal_projection for real inner product spaces, onto the direction of the affine subspace being projected onto.

Equations

euclidean_geometry.orthogonal_projection s = {to_fun := λ (p : P), ⟨euclidean_geometry.orthogonal_projection_fn s p, _⟩, linear := ↑(orthogonal_projection s.direction), map_vadd' := _}

source

@[simp]

theorem euclidean_geometry.orthogonal_projection_fn_eq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

euclidean_geometry.orthogonal_projection_fn s p = ↑(⇑(euclidean_geometry.orthogonal_projection s) p)

source

@[simp]

theorem euclidean_geometry.orthogonal_projection_linear {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] :

(euclidean_geometry.orthogonal_projection s).linear = ↑(orthogonal_projection s.direction)

The linear map corresponding to orthogonal_projection.

source

theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

↑s ∩ ↑(affine_subspace.mk' p (s.direction)ᗮ) = {↑(⇑(euclidean_geometry.orthogonal_projection s) p)}

The intersection of the subspace and the orthogonal subspace through the given point is the orthogonal_projection of that point onto the subspace.

source

theorem euclidean_geometry.orthogonal_projection_mem {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

↑(⇑(euclidean_geometry.orthogonal_projection s) p) ∈ s

The orthogonal_projection lies in the given subspace.

source

theorem euclidean_geometry.orthogonal_projection_mem_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

↑(⇑(euclidean_geometry.orthogonal_projection s) p) ∈ affine_subspace.mk' p (s.direction)ᗮ

The orthogonal_projection lies in the orthogonal subspace.

source

theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :

↑(⇑(euclidean_geometry.orthogonal_projection s) p2 -ᵥ ⟨p1, hp1⟩) ∈ s.direction

Subtracting a point in the given subspace from the orthogonal_projection produces a result in the direction of the given subspace.

source

theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :

↑(⟨p1, hp1⟩ -ᵥ ⇑(euclidean_geometry.orthogonal_projection s) p2) ∈ s.direction

Subtracting the orthogonal_projection from a point in the given subspace produces a result in the direction of the given subspace.

source

theorem euclidean_geometry.orthogonal_projection_eq_self_iff {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p : P} :

↑(⇑(euclidean_geometry.orthogonal_projection s) p) = p ↔ p ∈ s

A point equals its orthogonal projection if and only if it lies in the subspace.

source

@[simp]

theorem euclidean_geometry.orthogonal_projection_mem_subspace_eq_self {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : ↥s) :

⇑(euclidean_geometry.orthogonal_projection s) ↑p = p

source

@[simp]

theorem euclidean_geometry.orthogonal_projection_orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

⇑(euclidean_geometry.orthogonal_projection s) ↑(⇑(euclidean_geometry.orthogonal_projection s) p) = ⇑(euclidean_geometry.orthogonal_projection s) p

Orthogonal projection is idempotent.

source

theorem euclidean_geometry.eq_orthogonal_projection_of_eq_subspace {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s s' : affine_subspace ℝ P} [nonempty ↥s] [nonempty ↥s'] [complete_space ↥(s.direction)] [complete_space ↥(s'.direction)] (h : s = s') (p : P) :

↑(⇑(euclidean_geometry.orthogonal_projection s) p) = ↑(⇑(euclidean_geometry.orthogonal_projection s') p)

source

theorem euclidean_geometry.dist_orthogonal_projection_eq_zero_iff {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p : P} :

has_dist.dist p ↑(⇑(euclidean_geometry.orthogonal_projection s) p) = 0 ↔ p ∈ s

The distance to a point's orthogonal projection is 0 iff it lies in the subspace.

source

theorem euclidean_geometry.dist_orthogonal_projection_ne_zero_of_not_mem {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p : P} (hp : p ∉ s) :

has_dist.dist p ↑(⇑(euclidean_geometry.orthogonal_projection s) p) ≠ 0

The distance between a point and its orthogonal projection is nonzero if it does not lie in the subspace.

source

theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

↑(⇑(euclidean_geometry.orthogonal_projection s) p) -ᵥ p ∈ (s.direction)ᗮ

Subtracting p from its orthogonal_projection produces a result in the orthogonal direction.

source

theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction_orthogonal {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

p -ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p) ∈ (s.direction)ᗮ

Subtracting the orthogonal_projection from p produces a result in the orthogonal direction.

source

theorem euclidean_geometry.orthogonal_projection_vsub_orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

⇑(orthogonal_projection s.direction) (p -ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p)) = 0

Subtracting the orthogonal_projection from p produces a result in the kernel of the linear part of the orthogonal projection.

source

theorem euclidean_geometry.orthogonal_projection_vadd_eq_self {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ (s.direction)ᗮ) :

⇑(euclidean_geometry.orthogonal_projection s) (v +ᵥ p) = ⟨p, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector was in the orthogonal direction.

source

theorem euclidean_geometry.orthogonal_projection_vadd_smul_vsub_orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p1 : P} (p2 : P) (r : ℝ) (hp : p1 ∈ s) :

⇑(euclidean_geometry.orthogonal_projection s) (r • (p2 -ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p2)) +ᵥ p1) = ⟨p1, hp⟩

Adding a vector to a point in the given subspace, then taking the orthogonal projection, produces the original point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

source

theorem euclidean_geometry.dist_sq_eq_dist_orthogonal_projection_sq_add_dist_orthogonal_projection_sq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p1 : P} (p2 : P) (hp1 : p1 ∈ s) :

has_dist.dist p1 p2 * has_dist.dist p1 p2 = has_dist.dist p1 ↑(⇑(euclidean_geometry.orthogonal_projection s) p2) * has_dist.dist p1 ↑(⇑(euclidean_geometry.orthogonal_projection s) p2) + has_dist.dist p2 ↑(⇑(euclidean_geometry.orthogonal_projection s) p2) * has_dist.dist p2 ↑(⇑(euclidean_geometry.orthogonal_projection s) p2)

The square of the distance from a point in s to p2 equals the sum of the squares of the distances of the two points to the orthogonal_projection.

source

theorem euclidean_geometry.dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} {p1 p2 : P} (hp1 : p1 ∈ s) (hp2 : p2 ∈ s) (r1 r2 : ℝ) {v : V} (hv : v ∈ (s.direction)ᗮ) :

has_dist.dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) * has_dist.dist (r1 • v +ᵥ p1) (r2 • v +ᵥ p2) = has_dist.dist p1 p2 * has_dist.dist p1 p2 + (r1 - r2) * (r1 - r2) * (∥v∥ * ∥v∥)

The square of the distance between two points constructed by adding multiples of the same orthogonal vector to points in the same subspace.

source

noncomputable def euclidean_geometry.reflection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] :

P ≃ᵃⁱ[ℝ ] P

Reflection in an affine subspace, which is expected to be nonempty and complete. The word "reflection" is sometimes understood to mean specifically reflection in a codimension-one subspace, and sometimes more generally to cover operations such as reflection in a point. The definition here, of reflection in an affine subspace, is a more general sense of the word that includes both those common cases.

Equations

euclidean_geometry.reflection s = affine_isometry_equiv.mk' (λ (p : P), ↑(⇑(euclidean_geometry.orthogonal_projection s) p) -ᵥ p +ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p)) (reflection s.direction) ↑(classical.arbitrary ↥s) _

source

theorem euclidean_geometry.reflection_apply {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

⇑(euclidean_geometry.reflection s) p = ↑(⇑(euclidean_geometry.orthogonal_projection s) p) -ᵥ p +ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p)

The result of reflecting.

source

theorem euclidean_geometry.eq_reflection_of_eq_subspace {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s s' : affine_subspace ℝ P} [nonempty ↥s] [nonempty ↥s'] [complete_space ↥(s.direction)] [complete_space ↥(s'.direction)] (h : s = s') (p : P) :

⇑(euclidean_geometry.reflection s) p = ⇑(euclidean_geometry.reflection s') p

source

@[simp]

theorem euclidean_geometry.reflection_reflection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

⇑(euclidean_geometry.reflection s) (⇑(euclidean_geometry.reflection s) p) = p

Reflecting twice in the same subspace.

source

@[simp]

theorem euclidean_geometry.reflection_symm {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] :

(euclidean_geometry.reflection s).symm = euclidean_geometry.reflection s

Reflection is its own inverse.

source

theorem euclidean_geometry.reflection_involutive {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] :

function.involutive ⇑(euclidean_geometry.reflection s)

Reflection is involutive.

source

theorem euclidean_geometry.reflection_eq_self_iff {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] (p : P) :

⇑(euclidean_geometry.reflection s) p = p ↔ p ∈ s

A point is its own reflection if and only if it is in the subspace.

source

theorem euclidean_geometry.reflection_eq_iff_orthogonal_projection_eq {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s₁ s₂ : affine_subspace ℝ P) [nonempty ↥s₁] [nonempty ↥s₂] [complete_space ↥(s₁.direction)] [complete_space ↥(s₂.direction)] (p : P) :

⇑(euclidean_geometry.reflection s₁) p = ⇑(euclidean_geometry.reflection s₂) p ↔ ↑(⇑(euclidean_geometry.orthogonal_projection s₁) p) = ↑(⇑(euclidean_geometry.orthogonal_projection s₂) p)

Reflecting a point in two subspaces produces the same result if and only if the point has the same orthogonal projection in each of those subspaces.

source

theorem euclidean_geometry.dist_reflection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] (p₁ p₂ : P) :

has_dist.dist p₁ (⇑(euclidean_geometry.reflection s) p₂) = has_dist.dist (⇑(euclidean_geometry.reflection s) p₁) p₂

The distance between p₁ and the reflection of p₂ equals that between the reflection of p₁ and p₂.

source

theorem euclidean_geometry.dist_reflection_eq_of_mem {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (s : affine_subspace ℝ P) [nonempty ↥s] [complete_space ↥(s.direction)] {p₁ : P} (hp₁ : p₁ ∈ s) (p₂ : P) :

has_dist.dist p₁ (⇑(euclidean_geometry.reflection s) p₂) = has_dist.dist p₁ p₂

A point in the subspace is equidistant from another point and its reflection.

source

theorem euclidean_geometry.reflection_mem_of_le_of_mem {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s₁ s₂ : affine_subspace ℝ P} [nonempty ↥s₁] [complete_space ↥(s₁.direction)] (hle : s₁ ≤ s₂) {p : P} (hp : p ∈ s₂) :

⇑(euclidean_geometry.reflection s₁) p ∈ s₂

The reflection of a point in a subspace is contained in any larger subspace containing both the point and the subspace reflected in.

source

theorem euclidean_geometry.reflection_orthogonal_vadd {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p : P} (hp : p ∈ s) {v : V} (hv : v ∈ (s.direction)ᗮ) :

⇑(euclidean_geometry.reflection s) (v +ᵥ p) = -v +ᵥ p

Reflecting an orthogonal vector plus a point in the subspace produces the negation of that vector plus the point.

source

theorem euclidean_geometry.reflection_vadd_smul_vsub_orthogonal_projection {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : affine_subspace ℝ P} [nonempty ↥s] [complete_space ↥(s.direction)] {p₁ : P} (p₂ : P) (r : ℝ) (hp₁ : p₁ ∈ s) :

⇑(euclidean_geometry.reflection s) (r • (p₂ -ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p₂)) +ᵥ p₁) = -(r • (p₂ -ᵥ ↑(⇑(euclidean_geometry.orthogonal_projection s) p₂))) +ᵥ p₁

Reflecting a vector plus a point in the subspace produces the negation of that vector plus the point if the vector is a multiple of the result of subtracting a point's orthogonal projection from that point.

source

def euclidean_geometry.cospherical {P : Type u_2} [metric_space P] (ps : set P) :

Prop

A set of points is cospherical if they are equidistant from some point. In two dimensions, this is the same thing as being concyclic.

Equations

euclidean_geometry.cospherical ps = ∃ (center : P) (radius : ℝ), ∀ (p : P), p ∈ ps → has_dist.dist p center = radius

source

theorem euclidean_geometry.cospherical_def {P : Type u_2} [metric_space P] (ps : set P) :

euclidean_geometry.cospherical ps ↔ ∃ (center : P) (radius : ℝ), ∀ (p : P), p ∈ ps → has_dist.dist p center = radius

The definition of cospherical.

source

theorem euclidean_geometry.cospherical_subset {P : Type u_2} [metric_space P] {ps₁ ps₂ : set P} (hs : ps₁ ⊆ ps₂) (hc : euclidean_geometry.cospherical ps₂) :

euclidean_geometry.cospherical ps₁

A subset of a cospherical set is cospherical.

source

theorem euclidean_geometry.cospherical_empty {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] :

euclidean_geometry.cospherical ∅

The empty set is cospherical.

source

theorem euclidean_geometry.cospherical_singleton {P : Type u_2} [metric_space P] (p : P) :

euclidean_geometry.cospherical {p}

A single point is cospherical.

source

theorem euclidean_geometry.cospherical_pair {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] (p₁ p₂ : P) :

euclidean_geometry.cospherical {p₁, p₂}

Two points are cospherical.

source

theorem euclidean_geometry.cospherical.affine_independent {V : Type u_1} {P : Type u_2} [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P] {s : set P} (hs : euclidean_geometry.cospherical s) {p : fin 3 → P} (hps : set.range p ⊆ s) (hpi : function.injective p) :

affine_independent ℝ p

Any three points in a cospherical set are affinely independent.

mathlib documentation

Euclidean spaces #

Main definitions #

Implementation notes #

References #

Geometrical results on real inner product spaces #

Geometrical results on Euclidean affine spaces #