final_const_of_isTerminal — Mathlib

English

The inclusion of a terminal object is final.

Русский

Включение терминального объекта является финальным.

LaTeX

$$$\\mathrm{Final}(\\mathrm{Functor}.\\mathrm{const}\\; C\\, X)$ where X is a terminal object$$

Lean4

/-- The inclusion of a terminal object is final. -/
theorem final_const_of_isTerminal [IsFiltered C] {X : D} (hX : IsTerminal X) : ((Functor.const C).obj X).Final :=
  Functor.final_of_exists_of_isFiltered _ (fun _ => ⟨IsFiltered.nonempty.some, ⟨hX.from _⟩⟩)
    (fun {_ c} _ _ => ⟨c, 𝟙 _, hX.hom_ext _ _⟩)

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