symmetric_isOrtho

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

English

The IsOrtho relation is symmetric: if U ⟂ V then V ⟂ U.

Русский

Отношение IsOrtho симметрично: если U ⟂ V, то V ⟂ U.

LaTeX

$$Symmetric(IsOrtho)$$

Lean4

theorem symmetric_isOrtho : Symmetric (IsOrtho : Submodule 𝕜 E → Submodule 𝕜 E → Prop) := fun _ _ => IsOrtho.symm

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

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

Разделы

Аффилиация

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