final_iff_comp_equivalence — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See also the strictly more general `final_iff_comp_final_full_faithful` below. -/
theorem final_iff_comp_equivalence [IsEquivalence G] : Final F ↔ Final (F ⋙ G) :=
  ⟨fun _ => final_comp_equivalence _ _, fun _ => final_of_comp_full_faithful _ G⟩

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