English
If K1 ⊆ K2 and finrank K2 = finrank K1 + n, then finrank(K1⊥ ∩ K2) = n.
Русский
Если K1 ⊆ K2 и finrank K2 = finrank K1 + n, то finrank(K1⊥ ∩ K2) = n.
LaTeX
$$$ \text{If } K_1 \le K_2 \text{ and } \operatorname{finrank} K_2 = \operatorname{finrank} K_1 + n, \ \ \operatorname{finrank}(K_1^{\perp} \cap K_2) = n. $$$
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₂) {n : ℕ}
(h_dim : finrank 𝕜 K₁ + n = finrank 𝕜 K₂) : finrank 𝕜 (K₁ᗮ ⊓ K₂ : Submodule 𝕜 E) = n :=
by
rw [← add_right_inj (finrank 𝕜 K₁)]
simp [Submodule.finrank_add_inf_finrank_orthogonal h, h_dim]