mem_orthogonal_singleton_iff_inner_right

English

A vector v is in the orthogonal of the span of u (singleton) iff ⟪u, v⟫ = 0.

Русский

Вектор v ∈ (𝕜·u)⊥ тогда и только тогда, когда ⟪u, v⟫ = 0.

LaTeX

$$$$ v \in \operatorname{span}(u)^{\perp} \iff \langle u, v \rangle = 0. $$$$

Lean4

/-- A vector is in `(𝕜 ∙ u)ᗮ` iff it is orthogonal to `u`. -/
theorem mem_orthogonal_singleton_iff_inner_right {u v : E} : v ∈ (𝕜 ∙ u)ᗮ ↔ ⟪u, v⟫ = 0 :=
  by
  refine ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), ?_⟩
  intro hv w hw
  rw [mem_span_singleton] at hw
  obtain ⟨c, rfl⟩ := hw
  simp [inner_smul_left, hv]

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