isOrtho_top_left

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

English

⊤ ⟂ V iff V = ⊥.

Русский

⊤ ⟂ V эквивалентно V = ⊥.

LaTeX

$$\top \perp V \iff V = \bot$$

Lean4

@[simp]
theorem isOrtho_top_left {V : Submodule 𝕜 E} : ⊤ ⟂ V ↔ V = ⊥ :=
  isOrtho_comm.trans isOrtho_top_right

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

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

Разделы

Аффилиация

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