ortho_comm

Mathlib.LinearAlgebra.BilinearForm.Orthogonal

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

English

If B is symmetric (IsSymm), orthogonality is symmetric: IsOrtho x y ↔ IsOrtho y x.

Русский

Если B симметрична (IsSymm), ортогональность симметрична: IsOrtho x y ↔ IsOrtho y x.

LaTeX

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

Lean4

theorem ortho_comm (H : B.IsSymm) {x y : M} : IsOrtho B x y ↔ IsOrtho B y x :=
  LinearMap.IsSymm.ortho_comm (isSymm_iff.1 H)

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

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

Разделы

Аффилиация

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