isCompl_span_singleton_orthogonal

English

If a vector x is not self-orthogonal, the pair (span{x}, orthogonal(span{x})) is a complementary pair.

Русский

Если вектор x не самодортогонален, пара (span{x}, orthogonal(span{x})) образует комплементарную пару.

LaTeX

$$IsCompl(K \cdot x, B.orthogonal(K \cdot x))$$

Lean4

/-- Given a bilinear form `B` and some `x` such that `B x x ≠ 0`, the span of the singleton of `x`
  is complement to its orthogonal complement. -/
theorem isCompl_span_singleton_orthogonal {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
    IsCompl (K ∙ x) (B.orthogonal <| K ∙ x) :=
  { disjoint := disjoint_iff.2 <| span_singleton_inf_orthogonal_eq_bot hx
    codisjoint := codisjoint_iff.2 <| span_singleton_sup_orthogonal_eq_top hx }

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