initial_of_comp_full_faithful' — Mathlib

English

If G is full and faithful and Initial(F ⋙ G), then Initial(G).

Русский

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

LaTeX

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

Lean4

/-- The hypotheses also imply that `F` is initial, see `initial_of_comp_full_faithful`. -/
theorem initial_of_comp_full_faithful' [Full G] [Faithful G] [Initial (F ⋙ G)] : Initial G :=
  have := initial_of_comp_full_faithful F G
  initial_of_initial_comp F G

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