not_isOrtho_basis_self_of_separatingRight

English

An orthogonal basis with respect to a right-separating bilinear form has no self-orthogonal elements.

Русский

Базис, ортогональный относительно правого разделяющего отображения, не содержит самоугловых элементов.

LaTeX

$$∀ i, ¬B.IsOrtho (v i) (v i)$$

Lean4

/-- An orthogonal basis with respect to a right-separating bilinear map has no self-orthogonal
elements. -/
theorem not_isOrtho_basis_self_of_separatingRight [Nontrivial R] {B : M →ₛₗ[I] M →ₛₗ[I'] M₁} {v : Basis n R M}
    (h : B.IsOrthoᵢ v) (hB : B.SeparatingRight) (i : n) : ¬B.IsOrtho (v i) (v i) :=
  by
  rw [isOrthoᵢ_flip] at h
  rw [isOrtho_flip]
  exact h.not_isOrtho_basis_self_of_separatingLeft (flip_separatingLeft.mpr hB) i

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