mathlib documentation

geometry.euclidean.angle.unoriented.basic

Angles between vectors #

This file defines unoriented angles in real inner product spaces.

Main definitions #

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

The cosine of the angle between two vectors.

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

@[simp]

The angle between the negation of two vectors.

The angle between two vectors is nonnegative.

The angle between two vectors is at most π.

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

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

@[simp]

The angle between the zero vector and a vector.

@[simp]

The angle between a vector and the zero vector.

@[simp]

The angle between a nonzero vector and itself.

@[simp]

The angle between a nonzero vector and its negation.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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.

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.

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