initial_iff_comp_initial_full_faithful

English

If G is initial, full, and faithful, then Initial F is equivalent to Initial (F ⋙ G).

Русский

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

LaTeX

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

Lean4

theorem initial_iff_comp_initial_full_faithful [Initial G] [Full G] [Faithful G] : Initial F ↔ Initial (F ⋙ G) :=
  ⟨fun _ => initial_comp _ _, fun _ => initial_of_comp_full_faithful F G⟩

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