isOrtho_comm

Mathlib.Analysis.InnerProductSpace.Orthogonal

URI: https://scilib.ai/kg/mathlib#Submodule.isOrtho_comm

English

U ⟂ V if and only if V ⟂ U.

Русский

U ⟂ V, тогда и только тогда V ⟂ U.

LaTeX

$$$U \perp V \iff V \perp U$$$

Lean4

theorem isOrtho_comm {U V : Submodule 𝕜 E} : U ⟂ V ↔ V ⟂ U :=
  ⟨IsOrtho.symm, IsOrtho.symm⟩

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

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

Разделы

Аффилиация

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