incidenceSet_subset

Mathlib.Combinatorics.SimpleGraph.Subgraph

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

English

For any G' and v, G'.incidenceSet(v) is contained in G'.edgeSet.

Русский

Для любого подграфа G' и вершины v множествоincidenceSet содержится в edgeSet подграфа.

LaTeX

$$(G' : Subgraph G) (v : V) : G'.incidenceSet v ⊆ G'.edgeSet$$

Lean4

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

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

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

Разделы

Аффилиация

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