copyCount_le_labelledCopyCount

Mathlib.Combinatorics.SimpleGraph.Copy

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

← MathLib Explorer

English

⊤ ⊴ H iff ⊤ ⊑ H.

Русский

⊤ ⊴ H эквивалентно ⊤ ⊑ H.

LaTeX

$$$(\top : SimpleGraph V) \subseteq_{\mathrm{ind}} H \iff (\top : SimpleGraph V) \subseteq H$$$

Lean4

/-- There's at least as many labelled copies of `H` in `G` than unlabelled ones. -/
theorem copyCount_le_labelledCopyCount [Fintype W] : G.copyCount H ≤ G.labelledCopyCount H := by
  classical rw [copyCount_eq_card_image_copyToSubgraph]; exact card_image_le

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

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

Разделы

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

Аффилиация

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