cliqueFinset_mono

Mathlib.Combinatorics.SimpleGraph.Clique

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

English

If G ≤ H as graphs, then G.cliqueFinset n ⊆ H.cliqueFinset n.

Русский

Если граф G слабее чем H (G ≤ H), то n-клики G включены в n-клики H.

LaTeX

$$$G \\le H \\Rightarrow G.cliqueFinset n \\subseteq H.cliqueFinset n.$$$

Lean4

@[gcongr, mono]
theorem cliqueFinset_mono (h : G ≤ H) : G.cliqueFinset n ⊆ H.cliqueFinset n :=
  monotone_filter_right _ fun _ ↦ IsNClique.mono h

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

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

Разделы

Аффилиация

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