orthogonalFamily_self — Mathlib

English

The two-element family {K, K^⊥} forms an orthogonal family: any vector from K is orthogonal to any vector from K^⊥.

Русский

Пара подпространств {K, K^⊥} образует ортогональную семью: любые векторы из K и из K^⊥ взаимно ортогональны.

LaTeX

$$$\forall x \in K, \forall y \in K^{\perp}, \langle x, y \rangle = 0$$$

Lean4

theorem orthogonalFamily_self : OrthogonalFamily 𝕜 (fun b => ↥(cond b K Kᗮ)) fun b => (cond b K Kᗮ).subtypeₗᵢ
  | true, true => absurd rfl
  | true, false => fun _ x y => inner_right_of_mem_orthogonal x.prop y.prop
  | false, true => fun _ x y => inner_left_of_mem_orthogonal y.prop x.prop
  | false, false => absurd rfl

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