initial_of_equivalence_comp — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

/-- See also the strictly more general `initial_of_initial_comp` below. -/
theorem initial_of_equivalence_comp [IsEquivalence F] [Initial (F ⋙ G)] : Initial G where
  out d := isConnected_of_equivalent (CostructuredArrow.pre F G d).asEquivalence

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