graph_adjoint_toLinearPMap_eq_adjoint

English

If T has dense domain, the adjoint graph obtained as a LinearPMap equals the actual adjoint T†.

Русский

Если область определения T плотная, то граф сопряжения, полученный как LinearPMap, совпадает с сопряжением T†.

LaTeX

$$$T^{\\dagger}.\\mathrm{toLinearPMap} = T^{\\dagger}$, given dense domain$$

Lean4

@[simp]
theorem _root_.LinearPMap.graph_adjoint_toLinearPMap_eq_adjoint (hT : Dense (T.domain : Set E)) :
    T.graph.adjoint.toLinearPMap = T† := by
  apply eq_of_eq_graph
  rw [adjoint_graph_eq_graph_adjoint hT]
  apply Submodule.toLinearPMap_graph_eq
  intro x hx hx'
  simp only [mem_adjoint_iff, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, hx', inner_zero_right,
    zero_sub, neg_eq_zero, forall_exists_index, forall_apply_eq_imp_iff] at hx
  apply hT.eq_zero_of_inner_right
  rintro ⟨a, ha⟩
  exact hx a ha

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