ortho_comm

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

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

English

If B is reflexive, orthogonality is symmetric: IsOrtho x y ↔ IsOrtho y x.

Русский

Если B рефлексивна, ортогональность симметрична: IsOrtho x y ↔ IsOrtho y x.

LaTeX

$$$ B.IsRefl \\Rightarrow (B.IsOrtho x y \\iff B.IsOrtho y x) $$$

Lean4

theorem ortho_comm (H : B.IsRefl) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
  ⟨eq_zero H, eq_zero H⟩

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

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

Разделы

Аффилиация

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