Altitudes of a simplex #
This file defines the altitudes of a simplex and their feet.
Main definitions #
altitude
is the line that passes through a vertex of a simplex and is orthogonal to the opposite face.altitudeFoot
is the orthogonal projection of a vertex of a simplex onto the opposite face.height
is the distance between a vertex of a simplex and itsaltitudeFoot
.
References #
An altitude of a simplex is the line that passes through a vertex and is orthogonal to the opposite face.
Equations
- s.altitude i = AffineSubspace.mk' (s.points i) (affineSpan ℝ (s.points '' ↑(Finset.univ.erase i))).directionᗮ ⊓ affineSpan ℝ (Set.range s.points)
Instances For
The definition of an altitude.
A vertex lies in the corresponding altitude.
The direction of an altitude.
The vector span of the opposite face lies in the direction orthogonal to an altitude.
An altitude is finite-dimensional.
An altitude is one-dimensional (i.e., a line).
A line through a vertex is the altitude through that vertex if and only if it is orthogonal to the opposite face.
The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the opposite face.
Equations
- s.altitudeFoot i = ↑((s.faceOpposite i).orthogonalProjectionSpan (s.points i))
Instances For
The height of a vertex of a simplex is the distance between it and the foot of the altitude from that vertex.
Equations
- s.height i = dist (s.points i) (s.altitudeFoot i)