English
The finrank of the altitude direction is 1.
Русский
Размерность вектора направления высоты равна единице.
LaTeX
$$$\operatorname{finrank}_{\mathbb{R}}\big( (s.altitude(i)).\mathrm{direction} \big) = 1$$$
Lean4
/-- An altitude is one-dimensional (i.e., a line). -/
@[simp]
theorem finrank_direction_altitude {n : ℕ} [NeZero n] (s : Simplex ℝ P n) (i : Fin (n + 1)) :
finrank ℝ (s.altitude i).direction = 1 := by
rw [direction_altitude]
have h := Submodule.finrank_add_inf_finrank_orthogonal (vectorSpan_mono ℝ (Set.image_subset_range s.points { i }ᶜ))
have hn : (n - 1) + 1 = n := by
have := NeZero.ne n
cases n <;> omega
have hc : #({ i }ᶜ) = (n - 1) + 1 := by rw [card_compl, card_singleton, Fintype.card_fin, hn, add_tsub_cancel_right]
refine add_left_cancel (_root_.trans h ?_)
classical
rw [s.independent.finrank_vectorSpan (Fintype.card_fin _), ← Finset.coe_singleton, ← Finset.coe_compl, ←
Finset.coe_image, s.independent.finrank_vectorSpan_image_finset hc, hn]
