instNonempty

Mathlib.CategoryTheory.Groupoid.FreeGroupoid

URI: https://scilib.ai/kg/mathlib#Quiver.FreeGroupoid.instNonempty

English

For any nonempty quiver V, the free groupoid on V is nonempty.

Русский

Для непустого ориентированного графа V свободная группаoid содержит хотя бы один объект.

LaTeX

$$$\\text{Nonempty}(V) \\Rightarrow \\text{Nonempty}(\\text{FreeGroupoid } V)$$$

Lean4

instance {V} [Quiver V] [Nonempty V] : Nonempty (FreeGroupoid V) := by inhabit V; exact ⟨⟨@default V _⟩⟩

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

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

Разделы

Аффилиация

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