le_orthogonal_orthogonal

Mathlib.Analysis.InnerProductSpace.Orthogonal

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

English

For subspaces K1 and K2, K1^⊥ ∩ K2^⊥ = (K1 ⊔ K2)^⊥.

Русский

Для подпространств K1 и K2 выполняется: K1^⊥ ∩ K2^⊥ = (K1 ⊔ K2)^⊥.

LaTeX

$$$K_1^\perp \cap K_2^\perp = (K_1 \vee K_2)^\perp$$$

Lean4

/-- `K` is contained in `Kᗮᗮ`. -/
theorem le_orthogonal_orthogonal : K ≤ Kᗮᗮ :=
  (orthogonal_gc 𝕜 E).le_u_l _

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

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

Разделы

Аффилиация

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