final_const_terminal — Mathlib

English

The inclusion of a terminal object from the terminal in D is final for the constant functor.

Русский

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

LaTeX

$$$\\mathrm{Final}(\\mathrm{Functor}.\\mathrm{const}\\, C\\, (\\top_D))$$$

Lean4

/-- The inclusion of the terminal object is final. -/
theorem final_const_terminal [IsFiltered C] [HasTerminal D] : ((Functor.const C).obj (⊤_ D)).Final :=
  Functor.final_const_of_isTerminal terminalIsTerminal

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