ne_zero_of_not_isOrtho_self

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

URI: https://scilib.ai/kg/mathlib#LinearMap.BilinForm.ne_zero_of_not_isOrtho_self

English

If for x ∈ V we have not IsOrtho x x, then x ≠ 0.

Русский

Если для вектора x выписано, что x не ортогонален самому себе, то x ≠ 0.

LaTeX

$$$ \\neg B.IsOrtho(x,x) \\Rightarrow x \\neq 0 $$$

Lean4

theorem ne_zero_of_not_isOrtho_self {B : BilinForm K V} (x : V) (hx₁ : ¬B.IsOrtho x x) : x ≠ 0 := fun hx₂ =>
  hx₁ (hx₂.symm ▸ isOrtho_zero_left _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru