English
A basis that is orthogonal with respect to a left-separating bilinear form has no self-orthogonal basis vectors.
Русский
Базис, ортогональный относительно леворазделяющей билинейной формы, не может содержать вектора, ортогональные к самому себе.
LaTeX
$$∀ i, ¬ B.IsOrtho (v i) (v i)$$
Lean4
theorem nondegenerate_restrict_of_isCompl_ker {B : M →ₗ[R] M →ₗ[R] R} (hB : B.IsSymm) {W : Submodule R M}
(hW : IsCompl W (LinearMap.ker B)) : (B.domRestrict₁₂ W W).Nondegenerate :=
by
have hB' : (B.domRestrict₁₂ W W).IsRefl := fun x y ↦ hB.isRefl (W.subtype x) (W.subtype y)
rw [LinearMap.IsRefl.nondegenerate_iff_separatingLeft hB']
intro ⟨x, hx⟩ hx'
simp only [Submodule.mk_eq_zero]
replace hx' : ∀ y ∈ W, B x y = 0 := by simpa [Subtype.forall] using hx'
replace hx' : x ∈ W ⊓ ker B := by
refine ⟨hx, ?_⟩
ext y
obtain ⟨u, hu, v, hv, rfl⟩ : ∃ u ∈ W, ∃ v ∈ ker B, u + v = y := by rw [← Submodule.mem_sup, hW.sup_eq_top];
exact Submodule.mem_top
suffices B x u = 0 by rw [mem_ker] at hv; simpa [← hB.eq v, hv]
exact hx' u hu
simpa [hW.inf_eq_bot] using hx'
