emptyEquivalence

Mathlib.CategoryTheory.PEmpty

URI: https://scilib.ai/kg/mathlib#CategoryTheory.emptyEquivalence

Lean4

/-- Equivalence between two empty categories. -/
def emptyEquivalence : Discrete.{w} PEmpty ≌ Discrete.{v} PEmpty :=
  equivalenceOfIsEmpty _ _

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

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

Разделы

Аффилиация

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