initial_iff_comp_equivalence — Mathlib

English

If G is an equivalence, then Initial F is equivalent to Initial (F ⋙ G).

Русский

Если G — эквивалентность, то начальное F эквивалентно начальному (F ⋙ G).

LaTeX

$$$\operatorname{IsEquivalence}(G) \Rightarrow (\operatorname{Initial}(F) \iff \operatorname{Initial}(F \circ G))$$$

Lean4

/-- See also the strictly more general `initial_iff_comp_initial_full_faithful` below. -/
theorem initial_iff_comp_equivalence [IsEquivalence G] : Initial F ↔ Initial (F ⋙ G) :=
  ⟨fun _ => initial_comp_equivalence _ _, fun _ => initial_of_comp_full_faithful _ G⟩

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