restrict_nondegenerate_iff_isCompl_orthogonal

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⟩

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