le_ruzsaSzemerediNumber — Mathlib

English

If f embeds α into β, then ruzsaSzemerediNumber does not decrease under the induced map on graphs.

Русский

Если f встраивает α в β, то RS-число не убывает под соответствующим отображением графов.

LaTeX

$$$$ \\text{ruzsaSzemerediNumber}_α \\le \\text{ruzsaSzemerediNumber}_β \\text{ under embedding } f. $$$$

Lean4

theorem le_ruzsaSzemerediNumber [DecidableRel G.Adj] (hG : G.LocallyLinear) :
    #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α := by
  classical exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

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