isAdjointPair_iff_comp_eq_compl₂

English

IsAdjointPair B B' f g is equivalent to B'.comp f = B.compl₂ g.

Русский

Условие сопряжённости над B,B' эквивалентно равенству B'.comp f = B.compl₂ g.

LaTeX

$$$\text{IsAdjointPair}(B,B',f,g) \iff B'.comp f = B.compl_2\, g$$$

Lean4

theorem isAdjointPair_iff_comp_eq_compl₂ : IsAdjointPair B B' f g ↔ B'.comp f = B.compl₂ g :=
  by
  constructor <;> intro h
  · ext x y
    rw [comp_apply, compl₂_apply]
    exact h x y
  · intro _ _
    rw [← compl₂_apply, ← comp_apply, h]

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