spanningCoe_induce_le

Mathlib.Combinatorics.SimpleGraph.Maps

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

English

Inducing a graph to s and then spanningCoe back to V gives a subgraph of the original graph G.

Русский

Индукция к s, затем spanningCoe обратно к V, дают подграф исходного графа.

LaTeX

$$$ (\\mathrm{induce}(s, G)).\\mathrm{spanningCoe} \\le G $$$

Lean4

theorem spanningCoe_induce_le (s : Set V) : (G.induce s).spanningCoe ≤ G :=
  map_comap_le _ _

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

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

Разделы

Аффилиация

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