initial_iff_equivalence_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See also the strictly more general `initial_iff_initial_comp` below. -/
theorem initial_iff_equivalence_comp [IsEquivalence F] : Initial G ↔ Initial (F ⋙ G) :=
  ⟨fun _ => initial_equivalence_comp _ _, fun _ => initial_of_equivalence_comp F _⟩

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