ne_altitudeFoot — Mathlib

English

The altitude foot is never the vertex itself in a nondegenerate simplex.

Русский

Опорная точка высоты не совпадает с вершиной в неособенном симплексe.

LaTeX

$$$\forall n\, [NeZero n] (s:\text{Simplex }\mathbb{R} P\, n)\; \forall i, s.\text{points}(i) \neq s.\text{altitudeFoot}(i)$$$

Lean4

@[simp]
theorem ne_altitudeFoot {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) : s.points i ≠ s.altitudeFoot i :=
  by
  intro h
  rw [eq_comm, altitudeFoot, orthogonalProjectionSpan, orthogonalProjection_eq_self_iff] at h
  simp at h

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