orthogonal_disjoint — Mathlib

English

Two subspaces K and K⊥ have trivial intersection; they are disjoint in the lattice sense.

Русский

Подпространения K и K⊥ имеют тривиальное пересечение; они взаимно непересекаются в смысле анализа подмножеств.

LaTeX

$$$$ \text{Disjoint}(K, K^{\perp}). $$$$

Lean4

/-- `K` and `Kᗮ` have trivial intersection. -/
theorem orthogonal_disjoint : Disjoint K Kᗮ := by simp [disjoint_iff, K.inf_orthogonal_eq_bot]

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