English
In a space with a bilinear form B, if x is not self-orthogonal, then the intersection of the line spanned by x and its orthogonal complement is only {0}.
Русский
В пространстве с билинейной формой B, если x не самонирождён по отношению к B, то пересечение линейной области, порождаемой x, и её ортогонального дополнения равно {0}.
LaTeX
$$$ (K \cdot x) \cap B.orthogonal(K \cdot x) = \bot $$$
Lean4
theorem span_singleton_inf_orthogonal_eq_bot {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
(K ∙ x) ⊓ B.orthogonal (K ∙ x) = ⊥ := by
rw [← Finset.coe_singleton]
refine eq_bot_iff.2 fun y h => ?_
obtain ⟨μ, -, rfl⟩ := Submodule.mem_span_finset.1 h.1
have := h.2 x ?_
· rw [Finset.sum_singleton] at this ⊢
suffices hμzero : μ x = 0 by rw [hμzero, zero_smul, Submodule.mem_bot]
change B x (μ x • x) = 0 at this
rw [smul_right] at this
exact eq_zero_of_ne_zero_of_mul_right_eq_zero hx this
· rw [Submodule.mem_span]
exact fun _ hp =>
hp <|
Finset.mem_singleton_self
_
-- ↓ This lemma only applies in fields since we use the `mul_eq_zero`
