inf_orthogonal_self_le_ker_restrict

English

Any element in W ∩ B.orthogonal W maps to zero under the restricted bilinear form; hence lies in the kernel of B|W.

Русский

Любой элемент в W ∩ B.orthogonal W переходит в ноль под ограниченной билинейной формой, следовательно лежит в ядре B|W.

LaTeX

$$$W \cap B.orthogonal W \le \ker (B.restrict W)$$$

Lean4

theorem inf_orthogonal_self_le_ker_restrict {W : Submodule R M} (b₁ : B.IsRefl) :
    W ⊓ B.orthogonal W ≤ (LinearMap.ker <| B.restrict W).map W.subtype :=
  by
  rintro v ⟨hv : v ∈ W, hv' : v ∈ B.orthogonal W⟩
  simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coe_subtype, Subtype.exists, exists_and_left,
    exists_prop, exists_eq_right_right]
  refine ⟨?_, hv⟩
  ext ⟨w, hw⟩
  exact b₁ w v <| hv' w hw

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