Documentation

Mathlib.Geometry.Euclidean.Altitude

Altitudes of a simplex #

This file defines the altitudes of a simplex and their feet.

Main definitions #

References #

def Affine.Simplex.altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } (s : Simplex P (n + 1)) (i : Fin (n + 2)) :

An altitude of a simplex is the line that passes through a vertex and is orthogonal to the opposite face.

Equations
Instances For

    The definition of an altitude.

    theorem Affine.Simplex.mem_altitude {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } (s : Simplex P (n + 1)) (i : Fin (n + 2)) :

    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.

    @[simp]

    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.

    def Affine.Simplex.altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } [NeZero n] (s : Simplex P n) (i : Fin (n + 1)) :
    P

    The foot of an altitude is the orthogonal projection of a vertex of a simplex onto the opposite face.

    Equations
    Instances For
      @[simp]
      theorem Affine.Simplex.ne_altitudeFoot {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } [NeZero n] (s : Simplex P n) (i : Fin (n + 1)) :
      def Affine.Simplex.height {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } [NeZero n] (s : Simplex P n) (i : Fin (n + 1)) :

      The height of a vertex of a simplex is the distance between it and the foot of the altitude from that vertex.

      Equations
      Instances For
        theorem Affine.Simplex.height_pos {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace V] [MetricSpace P] [NormedAddTorsor V P] {n : } [NeZero n] (s : Simplex P n) (i : Fin (n + 1)) :
        0 < s.height i