finrank_orthogonal_span_singleton

English

If E is finite-dimensional and v ≠ 0, then finrank((𝕜 ∙ v)⊥) = finrank(E) - 1.

Русский

Если пространство E конечномерно и v ≠ 0, то размерность ортогонального дополнения span{v} равна finrank(E) − 1.

LaTeX

$$$ \operatorname{finrank}( (\mathbb{K} \cdot v)^{\perp} ) = \operatorname{finrank} E - 1. $$$

Lean4

/-- In a finite-dimensional inner product space, the dimension of the orthogonal complement of the
span of a nonzero vector is one less than the dimension of the space. -/
theorem finrank_orthogonal_span_singleton {n : ℕ} [_i : Fact (finrank 𝕜 E = n + 1)] {v : E} (hv : v ≠ 0) :
    finrank 𝕜 (𝕜 ∙ v)ᗮ = n := by
  haveI : FiniteDimensional 𝕜 E := .of_fact_finrank_eq_succ n
  exact finrank_add_finrank_orthogonal' <| by simp [finrank_span_singleton hv, _i.elim, add_comm]

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