verticesSet_nil

Mathlib.Combinatorics.Quiver.Path.Vertices

URI: https://scilib.ai/kg/mathlib#Quiver.Path.verticesSet_nil

← MathLib Explorer

English

The vertex set of the nil path from a to a is exactly {a}.

Русский

Множество вершин нулевого пути от a к a равно {a}.

LaTeX

$$verticesSet_nil$$

Lean4

theorem verticesSet_nil {a : V} : {v | v ∈ (nil : Path a a).vertices} = { a } :=
  by
  simp only [vertices_nil, mem_singleton, Set.ext_iff, Set.mem_singleton_iff]
  exact fun x ↦ Set.mem_setOf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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