Area of a triangle

This file collects formulas for the area of a triangle and other related results.

Main theorems

• Affine.Triangle.volume_eq_height_mul: $S = \frac{1}{2}hb$
• Affine.Triangle.volume_eq_mul_sin: $S = \frac{1}{2}ab \sin C$
• Affine.Triangle.volume_eq_sqrt_mul_sub_mul_sub_mul_sub: Heron's formula.

theorem Affine.Triangle.volume_eq_height_mul {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.volume t = 2⁻¹ * Simplex.height t i₁ * dist (t.points i₂) (t.points i₃)

theorem Affine.Triangle.volume_eq_mul_sin {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.volume t = 2⁻¹ * dist (t.points i₁) (t.points i₂) * dist (t.points i₂) (t.points i₃) * Real.sin (EuclideanGeometry.angle (t.points i₁) (t.points i₂) (t.points i₃))

theorem EuclideanGeometry.mul_sin_eq_sqrt_mul_sub_mul_sub_mul_sub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (p₁ p₂ p₃ : P) : 2⁻¹ * dist p₁ p₂ * dist p₂ p₃ * Real.sin (angle p₁ p₂ p₃) = √((dist p₁ p₂ + dist p₁ p₃ + dist p₂ p₃) / 2 * ((dist p₁ p₂ + dist p₁ p₃ + dist p₂ p₃) / 2 - dist p₁ p₂) * ((dist p₁ p₂ + dist p₁ p₃ + dist p₂ p₃) / 2 - dist p₁ p₃) * ((dist p₁ p₂ + dist p₁ p₃ + dist p₂ p₃) / 2 - dist p₂ p₃))

Heron's formula for possibly degenerate triangle. The area of a triangle with side lengths a, b, and c is √(s * (s - a) * (s - b) * (s - c)) where s = (a + b + c) / 2 is the semiperimeter. We show this by equating this formula to 2⁻¹ * a * c * sin γ, where γ is the angle opposite the side b.

theorem Affine.Triangle.volume_eq_sqrt_mul_sub_mul_sub_mul_sub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.volume t = √((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₁) (t.points i₂)) * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₁) (t.points i₃)) * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₂) (t.points i₃)))

Heron's formula for triangle. The area of a triangle with side lengths a, b, and c is √(s * (s - a) * (s - b) * (s - c)) where s = (a + b + c) / 2 is the semiperimeter.

theorem Affine.Triangle.volume_sq_eq_mul_sub_mul_sub_mul_sub {V : Type u_1} {P : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [MetricSpace P] [NormedAddTorsor V P] (t : Triangle ℝ P) {i₁ i₂ i₃ : Fin 3} (h₁₂ : i₁ ≠ i₂) (h₁₃ : i₁ ≠ i₃) (h₂₃ : i₂ ≠ i₃) : Simplex.volume t ^ 2 = (dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₁) (t.points i₂)) * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₁) (t.points i₃)) * ((dist (t.points i₁) (t.points i₂) + dist (t.points i₁) (t.points i₃) + dist (t.points i₂) (t.points i₃)) / 2 - dist (t.points i₂) (t.points i₃))