finrank_add_finrank_orthogonal — Mathlib

English

In the same setting as above, finrank(K1) + n = finrank(K2) implies finrank(K1⊥ ∩ K2) = n.

Русский

В той же постановке, если finrank(K1) + n = finrank(K2), то finrank(K1⊥ ∩ K2) = n.

LaTeX

$$$ \operatorname{finrank} K_1 + n = \operatorname{finrank} K_2 \implies \operatorname{finrank}(K_1^{\perp} \cap K_2) = n. $$$

Lean4

/-- Given a finite-dimensional space `E` and subspace `K`, the dimensions of `K` and `Kᗮ` add to
that of `E`. -/
theorem finrank_add_finrank_orthogonal [FiniteDimensional 𝕜 E] (K : Submodule 𝕜 E) :
    finrank 𝕜 K + finrank 𝕜 Kᗮ = finrank 𝕜 E :=
  by
  convert Submodule.finrank_add_inf_finrank_orthogonal (le_top : K ≤ ⊤) using 1
  · rw [inf_top_eq]
  · simp

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