direction_eq_vectorSpan — Mathlib

English

If the underlying set of an affine subspace is nonempty, then its direction matches its standard direction.

Русский

Если множество точек аффинного подпространства непусто, то направление совпадает с обычным направлением.

LaTeX

$$$directionOfNonempty h = s.direction$$$

Lean4

/-- The direction equals the `vectorSpan`. -/
theorem direction_eq_vectorSpan (s : AffineSubspace k P) : s.direction = vectorSpan k (s : Set P) :=
  rfl

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