span_singleton_sup_orthogonal_eq_top

English

If x is not self-orthogonal, the span of x together with its orthogonal complement spans the whole space.

Русский

Если x не самос ортогонален, тогда спан x вместе с его ортогональным дополнением порождают всё пространство.

LaTeX

$$$(K \cdot x) \;\;⊔\;\; B.orthogonal(K \cdot x) = \top$$$

Lean4

theorem span_singleton_sup_orthogonal_eq_top {B : BilinForm K V} {x : V} (hx : ¬B.IsOrtho x x) :
    (K ∙ x) ⊔ B.orthogonal (K ∙ x) = ⊤ :=
  by
  rw [orthogonal_span_singleton_eq_toLin_ker]
  exact LinearMap.span_singleton_sup_ker_eq_top _ hx

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