copyCount_eq_zero

Mathlib.Combinatorics.SimpleGraph.Copy

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

← MathLib Explorer

English

copyCount(G,H) = 0 if and only if H.Free G (no copy exists).

Русский

copyCount(G,H) = 0 тогда и только тогда, когда H не вложен в G (копий нет).

LaTeX

$$copyCount(G,H) = 0 \iff H.Free G$$

Lean4

@[simp]
theorem copyCount_eq_zero : G.copyCount H = 0 ↔ H.Free G := by
  simp [copyCount, Free, -nonempty_subtype, isContained_iff_exists_iso_subgraph, filter_eq_empty_iff]

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

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

Разделы

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

Аффилиация

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