isCompl_orthogonal_iff_disjoint — Mathlib

English

A subspace W yields a nondegenerate restriction of B if and only if W is complementary to its orthogonal with respect to B.

Русский

Подпространство W даёт недегнерированное ограничение B тогда и только тогда, когда W дополняет свою ортогональностью по B.

LaTeX

$$B.IsRefl → (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W)$$

Lean4

theorem isCompl_orthogonal_iff_disjoint (hB₀ : B.IsRefl) : IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W) :=
  by
  refine ⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩
  rw [codisjoint_iff]
  apply (eq_top_of_finrank_eq <| (finrank_le _).antisymm _)
  calc
    finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) := le_self_add
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W) := ?_
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) := by simp [h.eq_bot]
  rw [finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal hB₀ W]

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