finiteDimensional_direction_affineSpan_singleton

English

The direction of the affine span of a singleton is finite-dimensional.

Русский

Направление аффинного охвата одинокой точки конечномерно.

LaTeX

$$$\operatorname{FiniteDimensional}_k\bigl(\operatorname{direction}(\operatorname{affineSpan}_k\{p\})\bigr)$$$

Lean4

/-- The direction of the affine span of a singleton is finite-dimensional. -/
instance finiteDimensional_direction_affineSpan_singleton (p : P) :
    FiniteDimensional k (affineSpan k { p }).direction :=
  by
  rw [direction_affineSpan]
  infer_instance

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