final_of_equivalence_comp — Mathlib

English

If F: C → D is an equivalence and the composite F ⋙ G is final, then G is final.

Русский

Если F: C → D — эквивалентность и композиция F ⋙ G — финальная, то G финальная.

LaTeX

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

Lean4

/-- See also the strictly more general `final_of_final_comp` below. -/
theorem final_of_equivalence_comp [IsEquivalence F] [Final (F ⋙ G)] : Final G where
  out d := isConnected_of_equivalent (StructuredArrow.pre d F G).asEquivalence

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