final_iff_comp_final_full_faithful

English

If G is final, full, and faithful, then Final F is equivalent to Final (F ⋙ G).

Русский

Если G финальная, полная и верная, то Final F эквивален Final (F ⋙ G).

LaTeX

$$$\operatorname{Final}(G) \land \operatorname{Full}(G) \land \operatorname{Faithful}(G) \Rightarrow (\operatorname{Final}(F) \iff \operatorname{Final}(F \circ G))$$$

Lean4

theorem final_iff_comp_final_full_faithful [Final G] [Full G] [Faithful G] : Final F ↔ Final (F ⋙ G) :=
  ⟨fun _ => final_comp _ _, fun _ => final_of_comp_full_faithful F G⟩

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