English
For subspaces K1 ⊆ K2 in a finite-dimensional setting, finrank(K1) + finrank(K1⊥ ∩ K2) = finrank(K2).
Русский
Для подпространств K1 ⊆ K2 в конечномерном случае выполняется finrank(K1) + finrank(K1⊥ ∩ K2) = finrank(K2).
LaTeX
$$$ \operatorname{finrank} K_1 + \operatorname{finrank}(K_1^{\perp} \cap K_2) = \operatorname{finrank} K_2. $$$
Lean4
/-- Given a finite-dimensional subspace `K₂`, and a subspace `K₁`
contained in it, the dimensions of `K₁` and the intersection of its
orthogonal subspace with `K₂` add to that of `K₂`. -/
theorem finrank_add_inf_finrank_orthogonal {K₁ K₂ : Submodule 𝕜 E} [FiniteDimensional 𝕜 K₂] (h : K₁ ≤ K₂) :
finrank 𝕜 K₁ + finrank 𝕜 (K₁ᗮ ⊓ K₂ : Submodule 𝕜 E) = finrank 𝕜 K₂ :=
by
haveI : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h
haveI := FiniteDimensional.proper_rclike 𝕜 K₁
have hd := Submodule.finrank_sup_add_finrank_inf_eq K₁ (K₁ᗮ ⊓ K₂)
rw [← inf_assoc, (Submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection h] at hd
rw [add_zero] at hd
exact hd.symm
