finrank_add_finrank_orthogonal' — Mathlib

English

In the same framework, the equality of finranks across K1, K2, and their orthogonal intersection holds as in the previous statements.

Русский

В той же рамке равенство финерков между K1, K2 и их пересечением с ортогональным дополнением выполняется аналогично предыдущим утверждениям.

LaTeX

$$$ \operatorname{finrank}(K_1^{\perp} \cap K_2) = \operatorname{finrank} K_2 - \operatorname{finrank} K_1. $$$

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} {n : ℕ}
    (h_dim : finrank 𝕜 K + n = finrank 𝕜 E) : finrank 𝕜 Kᗮ = n :=
  by
  rw [← add_right_inj (finrank 𝕜 K)]
  simp [Submodule.finrank_add_finrank_orthogonal, h_dim]

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