Volume of a simplex

This file defines the volume of a simplex as Affine.Simplex.volume. It is kept thin and all lemmas are put to Mathlib.Geometry.Euclidean.Volume.MeasureSimplex (for connection to the volume measure) and Mathlib.Geometry.Euclidean.Volume.Basic (for lemmas outside of measure theory).

noncomputable def Affine.Simplex.volume {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] {n : ℕ} (s : Simplex ℝ P n) : ℝ

The volume of a n-dimensional simplex, internally defined using base-and-height formula from the 0-th vertex.

See also:

• Affine.Simplex.volume_eq_euclideanHausdorffMeasure_real_closedInterior for connection between the definition and the Euclidean Hausdorff measure.
• Affine.Simplex.volume_eq for the base-and-height formula from any vertex.

Equations

• s_2.volume = 1
• s_2.volume = (↑(n_2 + 1))⁻¹ * s_2.height 0 * (s_2.faceOpposite 0).volume