full_empty

Mathlib.CategoryTheory.Groupoid.Subgroupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Subgroupoid.full_empty

English

The full subgroupoid on the empty set equals the bottom subgroupoid.

Русский

Полная подгруппоида на пустом множестве равна нижнему подгруппоида.

LaTeX

$$$full \\ emptyset = (⊥ : Subgroupoid C)$$$

Lean4

@[simp]
theorem full_empty : full ∅ = (⊥ : Subgroupoid C) := by
  ext
  simp only [Bot.bot, mem_full_iff, mem_empty_iff_false, and_self_iff]

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

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

Разделы

Аффилиация

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