affineSpan_pair_altitudeFoot_eq_altitude

English

As above, the altitudeFoot equality for a simplex reappears in the same setup, asserting the equality of the affine span built from altitudeFoot and the vertex set with the altitude at i.

Русский

Как и ранее, повторяется равенство аффинного span, полученного из altitudeFoot и набора вершин, с высотой s в точке i.

LaTeX

$$$$ \\text{affineSpan Real (\\{altitudeFoot i, points i\\})} = altitude(i) $$$$

Lean4

theorem affineSpan_pair_altitudeFoot_eq_altitude {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    line[ℝ, s.altitudeFoot i, s.points i] = s.altitude i :=
  by
  rw [affineSpan_pair_eq_altitude_iff]
  refine ⟨(s.ne_altitudeFoot i).symm, s.altitudeFoot_mem_affineSpan _, ?_⟩
  rw [altitudeFoot, orthogonalProjectionSpan]
  simp_rw [range_faceOpposite_points]
  exact orthogonalProjection_vsub_mem_direction_orthogonal _ _

Похожие утверждения