ortho_comm

Mathlib.LinearAlgebra.SesquilinearForm.Basic

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

English

If B is alternating, then orthogonality is symmetric: IsOrho x y iff IsOrho y x.

Русский

Если B чередующаяся, ортогональность симметрична: IsOrtho x y ⇔ IsOrtho y x.

LaTeX

$$$\text{IsAlt}(B) \Rightarrow \forall x,y,\ IsOrtho x y \iff IsOrtho y x$$$

Lean4

theorem ortho_comm (H : B.IsAlt) {x y} : IsOrtho B x y ↔ IsOrtho B y x :=
  H.isRefl.ortho_comm

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

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

Разделы

Аффилиация

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