toLin_restrict_range_dualCoannihilator_eq_orthogonal

English

The dual coannihilator of the range of B restricted to W equals the orthogonal to W.

Русский

Дуал-коаннигилятор образа B на W совпадает с B.orthogonal(W).

LaTeX

$$$(\operatorname{range}(B. domRestrict W)).dualCoannihilator = B.orthogonal W$$$

Lean4

theorem toLin_restrict_range_dualCoannihilator_eq_orthogonal (B : BilinForm K V) (W : Subspace K V) :
    (LinearMap.range (B.domRestrict W)).dualCoannihilator = B.orthogonal W :=
  by
  ext x; constructor <;> rw [mem_orthogonal_iff] <;> intro hx
  · intro y hy
    rw [Submodule.mem_dualCoannihilator] at hx
    exact hx (B.domRestrict W ⟨y, hy⟩) ⟨⟨y, hy⟩, rfl⟩
  · rw [Submodule.mem_dualCoannihilator]
    rintro _ ⟨⟨w, hw⟩, rfl⟩
    exact hx w hw

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