killCopies_le_left

Mathlib.Combinatorics.SimpleGraph.Copy

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

← MathLib Explorer

English

The result of killCopies is a subgraph of G: G.killCopies H ≤ G.

Русский

Результат killCopies является подграфом G: G.killCopies H ≤ G.

LaTeX

$$G.killCopies(H) \le G$$

Lean4

/-- Removing an edge from `G` for each subgraph isomorphic to `H` results in a subgraph of `G`. -/
theorem killCopies_le_left : G.killCopies H ≤ G := by rw [killCopies]; split_ifs; exacts [le_rfl, deleteEdges_le _]

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

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

Разделы

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

Аффилиация

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