Theorems · Theorem · geometry

Affine.Simplex.affineSpan_pair_eq_altitude_iff

∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [NeZero n] (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)) (p : P),
  line[ℝ, p, s.points i] = s.altitude i ↔
    p ≠ s.points i ∧
      p ∈ affineSpan ℝ (Set.range s.points) ∧ p -ᵥ s.points i ∈ (affineSpan ℝ (s.points '' {i}ᶜ)).directionᗮ

A line through a vertex is the altitude through that vertex if and only if it is orthogonal to the opposite face.

Defined in

Mathlib.Geometry.Euclidean.Altitude

Cited by

2 results in Mathlib

Foundations

Depth 182 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceMetricSpaceNormedAddTorsorNeZero