isOrtho_self

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

← MathLib Explorer

English

A submodule U is orthogonal to itself if and only if U is the zero submodule.

Русский

Подмодуль U ортогонален самому себе тогда и только тогда, когда U = ⊥.

LaTeX

$$$U \perp U \;\iff\; U = \{0\}$$$

Lean4

@[simp]
theorem isOrtho_self {U : Submodule 𝕜 E} : U ⟂ U ↔ U = ⊥ :=
  ⟨fun h => eq_bot_iff.mpr fun x hx => inner_self_eq_zero.mp (h hx x hx), fun h => h.symm ▸ isOrtho_bot_left⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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