finrank_add_inf_finrank_orthogonal'

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]

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