English
A subspace restriction is nondegenerate if and only if the subspace is complementary to its orthogonal.
Русский
Ограничение недегнерируемо тогда и только тогда, когда подпространство комплементарно своей ортогонали.
LaTeX
$$restrict_nondegenerate_iff_isCompl_orthogonal b₁ : (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W)$$
Lean4
/-- A subspace is complement to its orthogonal complement with respect to some reflexive bilinear
form if and only if that bilinear form restricted on to the subspace is nondegenerate. -/
theorem restrict_nondegenerate_iff_isCompl_orthogonal (b₁ : B.IsRefl) :
(B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W) :=
⟨fun b₂ => isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂, fun h =>
B.nondegenerate_restrict_of_disjoint_orthogonal b₁ h.1⟩