finrank_add_finrank_orthogonal — Mathlib

English

If x is not self-orthogonal, the span of x and its orthogonal is a direct complement.

Русский

Если x не самор-ортогонален,span{x} и его ортогональное дополнение образуют прямое дополнение.

LaTeX

$$Not (B.IsOrtho x x) → IsCompl(K \cdot x, B.orthogonal(K \cdot x))$$

Lean4

theorem finrank_add_finrank_orthogonal (b₁ : B.IsRefl) (W : Submodule K V) :
    finrank K W + finrank K (B.orthogonal W) = finrank K V + finrank K (W ⊓ B.orthogonal ⊤ : Subspace K V) :=
  by
  rw [← toLin_restrict_ker_eq_inf_orthogonal _ _ b₁, ← toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _,
    finrank_map_subtype_eq]
  conv_rhs =>
    rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _ (LinearMap.range (B.domRestrict W)), add_comm,
      ← add_assoc, add_comm (finrank K (LinearMap.ker (B.domRestrict W))), LinearMap.finrank_range_add_finrank_ker]

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