inhabited

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CommaMorphism.inhabited

Lean4

instance inhabited [Inhabited (Comma L R)] : Inhabited (CommaMorphism (default : Comma L R) default) :=
  ⟨{ left := 𝟙 _, right := 𝟙 _ }⟩

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

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

Разделы

Аффилиация

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