vectorSpan_isOrtho_altitude_direction

English

The vector span of the opposite face is orthogonal to the altitude's direction.

Русский

Векторный спан противоположной грани ортогонален направлению высоты.

LaTeX

$$$\operatorname{vectorSpan}_{\mathbb{R}}\left( s.points''{ i }^c \right) \perp ( s.altitude(i) ).\mathrm{direction}$$$

Lean4

/-- The vector span of the opposite face lies in the direction
orthogonal to an altitude. -/
theorem vectorSpan_isOrtho_altitude_direction {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    vectorSpan ℝ (s.points '' { i }ᶜ) ⟂ (s.altitude i).direction :=
  by
  rw [direction_altitude]
  exact (Submodule.isOrtho_orthogonal_right _).mono_right inf_le_left

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