altitudeFoot_mem_altitude — Mathlib

English

Let s be a simplex and i an index of a vertex. The foot of the altitude from vertex i lies on the altitude corresponding to i; i.e., AltitudeFoot_i lies in Altitude_i.

Русский

Пусть s — симплекс и i — индекс вершины. Опорная точка высоты из вершины i принадлежит самой высоте относительно i; то есть AltitudeFoot_i ∈ Altitude_i.

LaTeX

$$$s\\!:\\operatorname{altitudeFoot}(i) \\in s\\!:\\operatorname{altitude}(i)$$$

Lean4

theorem altitudeFoot_mem_altitude {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    s.altitudeFoot i ∈ s.altitude i :=
  by
  rw [← affineSpan_pair_altitudeFoot_eq_altitude]
  exact left_mem_affineSpan_pair _ _ _

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