direction_bot — Mathlib

English

The direction of the bottom affine subspace is the bottom subspace.

Русский

Направление нижнего аффинного подпро пространства равно нулевому подпространству.

LaTeX

$$$\operatorname{direction}(\bot) = \bot$$$

Lean4

/-- The direction of `⊥` is the submodule `⊥`. -/
@[simp]
theorem direction_bot : (⊥ : AffineSubspace k P).direction = ⊥ := by
  rw [direction_eq_vectorSpan, bot_coe, vectorSpan_def, vsub_empty, Submodule.span_empty]

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