incidenceFinset_subset

Mathlib.Combinatorics.SimpleGraph.Finite

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

← MathLib Explorer

English

The incidenceFinset v is a subset of the edgeFinset of G.

Русский

IncidenceFinset v является подмножество edgeFinset графа G.

LaTeX

$$$ G.incidenceFinset v \subseteq G.edgeFinset $$$

Lean4

theorem incidenceFinset_subset [DecidableEq V] [Fintype G.edgeSet] : G.incidenceFinset v ⊆ G.edgeFinset :=
  Set.toFinset_subset_toFinset.mpr (G.incidenceSet_subset v)

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

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

Разделы

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

Аффилиация

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