span_singleton_sup_orthogonal_eq_top

English

Under field assumptions, the intersection of the span of x with its orthogonal is {0} when B x x ≠ 0.

Русский

При полях, если B x x ≠ 0, пересечение порожденного x пространства и его ортогонального дополнения равно {0}.

LaTeX

$$$(K_1 \cdot x) \cap (K_1 \cdot x)^{⊥_B} = \{0\}$$$

Lean4

theorem span_singleton_sup_orthogonal_eq_top {B : V →ₗ[K] V →ₗ[K] K} {x : V} (hx : ¬B.IsOrtho x x) :
    (K ∙ x) ⊔ Submodule.orthogonalBilin (N := K ∙ x) (B := B) = ⊤ :=
  by
  rw [orthogonal_span_singleton_eq_to_lin_ker]
  exact (B x).span_singleton_sup_ker_eq_top hx

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