finiteDimensional_direction_altitude

English

The direction of an altitude is finite-dimensional over the base ring.

Русский

Направление высоты имеет конечную размерность над основанием.

LaTeX

$$$\mathrm{FiniteDimensional}_{\mathbb{R}}\big( (s.altitude(i)).\mathrm{direction} \big)$$$

Lean4

/-- An altitude is finite-dimensional. -/
instance finiteDimensional_direction_altitude {n : ℕ} (s : Simplex ℝ P n) (i : Fin (n + 1)) :
    FiniteDimensional ℝ (s.altitude i).direction :=
  by
  rw [direction_altitude]
  infer_instance

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