final_of_comp_full_faithful — Mathlib

English

If G is full and faithful and F ⋙ G is final, then F is final.

Русский

Если G полон и верен и F ⋙ G финален, тогда F финален.

LaTeX

$$$[\\text{Full}(G)] \\wedge [\\text{Faithful}(G)] \\wedge [\\text{Final}(F \\circ G)] \\Rightarrow [\\text{Final}(F)].$$$

Lean4

/-- The hypotheses also imply that `G` is final, see `final_of_comp_full_faithful'`. -/
theorem final_of_comp_full_faithful [Full G] [Faithful G] [Final (F ⋙ G)] : Final F where
  out d := isConnected_of_equivalent (StructuredArrow.post d F G).asEquivalence.symm

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