disjoint

Mathlib.Analysis.InnerProductSpace.Orthogonal

URI: https://scilib.ai/kg/mathlib#Submodule.IsOrtho.disjoint

← MathLib Explorer

English

Orthogonality implies disjointness: if U ⟂ V, then U ∩ V = {0}.

Русский

Ортогональность влечет за собой дискjointness: если U ⟂ V, то U ∩ V = {0}.

LaTeX

$$$(U \perp V) \Rightarrow (U \cap V = \{0\})$$$

Lean4

/-- Orthogonal submodules are disjoint. -/
theorem disjoint {U V : Submodule 𝕜 E} (h : U ⟂ V) : Disjoint U V :=
  (Submodule.orthogonal_disjoint _).mono_right h.symm

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

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

Разделы

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

Аффилиация

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