mathlib documentation

geometry.euclidean.basic

Euclidean spaces #

This file makes some definitions and proves very basic geometrical results about real inner product spaces and Euclidean affine spaces. Results about real inner product spaces that involve the norm and inner product but not angles generally go in analysis.normed_space.inner_product. Results with longer proofs or more geometrical content generally go in separate files.

Main definitions #

Implementation notes #

To declare P as the type of points in a Euclidean affine space with V as the type of vectors, use [inner_product_space ℝ V] [metric_space P] [normed_add_torsor V P]. This works better with out_param to make V implicit in most cases than having a separate type alias for Euclidean affine spaces.

Rather than requiring Euclidean affine spaces to be finite-dimensional (as in the definition on Wikipedia), this is specified only for those theorems that need it.

References #

Geometrical results on Euclidean affine spaces #

This section develops some geometrical definitions and results on Euclidean affine spaces.

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

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.

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.

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.)

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.

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.

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).

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).

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

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.

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.

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.

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.

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

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

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

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

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

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

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

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

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.

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.

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.

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

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

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.

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

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

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₂) :

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

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

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.

theorem euclidean_geometry.sphere.ext {P : Type u_2} {_inst_2 : metric_space P} (x y : euclidean_geometry.sphere P) (h : x.center = y.center) (h_1 : x.radius = y.radius) :
x = y
@[ext]
structure euclidean_geometry.sphere (P : Type u_2) [metric_space P] :
Type u_2
  • center : P
  • radius :

A sphere P bundles a center and radius. This definition does not require the radius to be positive; that should be given as a hypothesis to lemmas that require it.

Instances for euclidean_geometry.sphere
theorem euclidean_geometry.sphere.mk_center {P : Type u_2} [metric_space P] (c : P) (r : ) :
{center := c, radius := r}.center = c
theorem euclidean_geometry.sphere.mk_radius {P : Type u_2} [metric_space P] (c : P) (r : ) :
{center := c, radius := r}.radius = r
@[simp]
theorem euclidean_geometry.sphere.coe_mk {P : Type u_2} [metric_space P] (c : P) (r : ) :
@[simp]
theorem euclidean_geometry.subset_sphere {P : Type u_2} [metric_space P] {ps : set P} {s : euclidean_geometry.sphere P} :
ps s (p : P), p ps p s
theorem euclidean_geometry.dist_of_mem_subset_sphere {P : Type u_2} [metric_space P] {p : P} {ps : set P} {s : euclidean_geometry.sphere P} (hp : p ps) (hps : ps s) :
theorem euclidean_geometry.dist_of_mem_subset_mk_sphere {P : Type u_2} [metric_space P] {p c : P} {ps : set P} {r : } (hp : p ps) (hps : ps {center := c, radius := r}) :
theorem euclidean_geometry.sphere.ne_iff {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} :
s₁ s₂ s₁.center s₂.center s₁.radius s₂.radius
theorem euclidean_geometry.sphere.center_eq_iff_eq_of_mem {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
s₁.center = s₂.center s₁ = s₂
theorem euclidean_geometry.sphere.center_ne_iff_ne_of_mem {P : Type u_2} [metric_space P] {s₁ s₂ : euclidean_geometry.sphere P} {p : P} (hs₁ : p s₁) (hs₂ : p s₂) :
s₁.center s₂.center s₁ s₂
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere {P : Type u_2} [metric_space P] {p₁ p₂ : P} {s : euclidean_geometry.sphere P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
theorem euclidean_geometry.dist_center_eq_dist_center_of_mem_sphere' {P : Type u_2} [metric_space P] {p₁ p₂ : P} {s : euclidean_geometry.sphere P} (hp₁ : p₁ s) (hp₂ : p₂ s) :
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
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.

A set of points is cospherical if and only if they lie in some sphere.

The set of points in a sphere is cospherical.

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

A subset of a cospherical set is cospherical.

A single point is cospherical.

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) :

Two points are cospherical.

Any three points in a cospherical set are affinely independent.

theorem euclidean_geometry.inner_vsub_vsub_of_mem_sphere_of_mem_sphere {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {p₁ p₂ : P} {s₁ s₂ : euclidean_geometry.sphere P} (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) :
has_inner.inner (s₂.center -ᵥ s₁.center) (p₂ -ᵥ p₁) = 0

Suppose that p₁ and p₂ lie in spheres s₁ and s₂. Then the vector between the centers of those spheres is orthogonal to that between p₁ and p₂; this is a version of inner_vsub_vsub_of_dist_eq_of_dist_eq for bundled spheres. (In two dimensions, this says that the diagonals of a kite are orthogonal.)

theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_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) {s₁ s₂ : euclidean_geometry.sphere P} {p₁ p₂ p : P} (hs₁ : s₁.center s) (hs₂ : s₂.center s) (hp₁s : p₁ s) (hp₂s : p₂ s) (hps : p s) (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
p = p₁ p = p₂

Two spheres intersect in at most two points in a two-dimensional subspace containing their centers; this is a version of eq_of_dist_eq_of_dist_eq_of_mem_of_finrank_eq_two for bundled spheres.

theorem euclidean_geometry.eq_of_mem_sphere_of_mem_sphere_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) {s₁ s₂ : euclidean_geometry.sphere P} {p₁ p₂ p : P} (hs : s₁ s₂) (hp : p₁ p₂) (hp₁s₁ : p₁ s₁) (hp₂s₁ : p₂ s₁) (hps₁ : p s₁) (hp₁s₂ : p₁ s₂) (hp₂s₂ : p₂ s₂) (hps₂ : p s₂) :
p = p₁ p = p₂

Two spheres intersect in at most two points in two-dimensional space; this is a version of eq_of_dist_eq_of_dist_eq_of_finrank_eq_two for bundled spheres.

structure euclidean_geometry.concyclic {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] (ps : set P) :
Prop

A set of points is concyclic if it is cospherical and coplanar. (Most results are stated directly in terms of cospherical instead of using concyclic.)

theorem euclidean_geometry.concyclic.subset {V : Type u_1} {P : Type u_2} [inner_product_space V] [metric_space P] [normed_add_torsor V P] {ps₁ ps₂ : set P} (hs : ps₁ ps₂) (h : euclidean_geometry.concyclic ps₂) :

A subset of a concyclic set is concyclic.

A single point is concyclic.

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

Two points are concyclic.