isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top

English

Equivalence: F.IsLeftAdjoint iff F.rightAdjointObjIsDefined = ⊤.

Русский

Эквивалентность: F является левым сопряжённым тогда и только тогда, когда F.rightAdjointObjIsDefined = ⊤.

LaTeX

$$$F.IsLeftAdjoint \iff F.rightAdjointObjIsDefined = \top$$$

Lean4

theorem isLeftAdjoint_iff_rightAdjointObjIsDefined_eq_top : F.IsLeftAdjoint ↔ F.rightAdjointObjIsDefined = ⊤ :=
  by
  refine ⟨fun h ↦ ?_, isLeftAdjoint_of_rightAdjointObjIsDefined_eq_top⟩
  ext X
  simpa only [Pi.top_apply, «Prop».top_eq_true, iff_true] using
    rightAdjointObjIsDefined_of_adjunction (Adjunction.ofIsLeftAdjoint F) X

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