final_iff_equivalence_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See also the strictly more general `final_iff_final_comp` below. -/
theorem final_iff_equivalence_comp [IsEquivalence F] : Final G ↔ Final (F ⋙ G) :=
  ⟨fun _ => final_equivalence_comp _ _, fun _ => final_of_equivalence_comp F _⟩

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