isCompl_span_singleton_orthogonal

English

The span of a single vector and its orthogonal complement form a complete direct sum.

Русский

Образ единственного вектора и его ортогональное дополнение образуют полный прямой прямой сумма.

LaTeX

$$IsCompl(Span{ x }, N^{⊥_B})$$

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 : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
    IsCompl (K ∙ x) (Submodule.orthogonalBilin (N := K ∙ x) (B := B)) :=
  { disjoint := disjoint_iff.2 <| span_singleton_inf_orthogonal_eq_bot B x hx
    codisjoint := codisjoint_iff.2 <| span_singleton_sup_orthogonal_eq_top hx }

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