English
If B is reflexive and B|W is nondegenerate and B.orthogonal W = ⊥, then W = ⊤.
Русский
Если B рефлексивна, ограничение B|W невdegenerate и B.orthogonal W = ⊥, тогда W = ⊤.
LaTeX
$$B.IsRefl → (B.restrict W).Nondegenerate → B.orthogonal W = ⊥ → W = ⊤$$
Lean4
/-- A subspace is complement to its orthogonal complement with respect to some
reflexive bilinear form if that bilinear form restricted on to the subspace is nondegenerate. -/
theorem isCompl_orthogonal_of_restrict_nondegenerate (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) :
IsCompl W (B.orthogonal W) :=
by
have : W ⊓ B.orthogonal W = ⊥ := by
rw [eq_bot_iff]
intro x hx
obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx
refine Subtype.mk_eq_mk.1 (b₂ ⟨x, hx₁⟩ ?_)
rintro ⟨n, hn⟩
simp only [restrict_apply, domRestrict_apply]
exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))
refine IsCompl.of_eq this (eq_top_of_finrank_eq <| (finrank_le _).antisymm ?_)
conv_rhs => rw [← add_zero (finrank K _)]
rw [← finrank_bot K V, ← this, finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal b₁]
exact le_self_add
