incidenceSet_subset

Mathlib.Combinatorics.SimpleGraph.Basic

URI: https://scilib.ai/kg/mathlib#SimpleGraph.incidenceSet_subset

English

For every vertex v, incidenceSet(v) is a subset of the edge set.

Русский

Для каждой вершины v incidenceSet(v) ⊆ edgeSet.

LaTeX

$$$\\forall v,\\ incidenceSet(v) \\subseteq G.\\mathrm{edgeSet}$$$

Lean4

theorem incidenceSet_subset (v : V) : G.incidenceSet v ⊆ G.edgeSet := fun _ h => h.1

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

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

Разделы

Аффилиация

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