preservesTerminalIso_id

Mathlib.CategoryTheory.Monoidal.Cartesian.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CartesianMonoidalCategory.preservesTerminalIso_id

English

Under the same hypotheses, the hom component of preservesTerminalIso equals terminalComparison.

Русский

При тех же предпосылках гомоморфизм сохраняющего терминал совпадает с terminalComparison.

LaTeX

$$(preservesTerminalIso F).hom = terminalComparison F$$

Lean4

@[simp]
theorem preservesTerminalIso_id : preservesTerminalIso (𝟭 C) = .refl _ := by cat_disch

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru