English
In a finite-dimensional setting with a nondegenerate reflexive bilinear form, the sum of the dimensions of a subspace W and its orthogonal equals the ambient space plus the dimension of their intersection with the orthogonal of the top.
Русский
В конечномерном случае с недегенерируемой рефлексивной билинейной формой сумма размерностей подпространства W и его ортогонального равна размерности всего пространства плюс размерность пересечения с B.orthogonal ⊤.
LaTeX
$$$\operatorname{finrank}_K (B.orthogonal W) = \operatorname{finrank}_K V - \operatorname{finrank}_K W$$$
Lean4
theorem finrank_orthogonal (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) :
finrank K (B.orthogonal W) = finrank K V - finrank K W :=
by
have := finrank_add_finrank_orthogonal hB₀ (W := W)
rw [B.orthogonal_top_eq_bot hB hB₀, inf_bot_eq, finrank_bot, add_zero] at this
cutsat
