ruzsaSzemerediNumber_spec — Mathlib

English

There exists a graph G whose 3-clique count equals the RS-number and which is locally linear.

Русский

Существует граф G, у которого число треугольников трёхклаковых равно RS-числу и граф локально линейный.

LaTeX

$$$$ \\exists G, (|\\text{cliqueFinset}(G,3)| = \\ ruzsaSzemerediNumber α) \\land G.\\text{LocallyLinear}. $$$$

Lean4

theorem ruzsaSzemerediNumber_spec :
    ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj), #(G.cliqueFinset 3) = ruzsaSzemerediNumber α ∧ G.LocallyLinear := by
  classical
    exact
    @Nat.findGreatest_spec _
      (fun m ↦ ∃ (G : SimpleGraph α) (_ : DecidableRel G.Adj), #(G.cliqueFinset 3) = m ∧ G.LocallyLinear) _ _
      (Nat.zero_le _) ⟨⊥, inferInstance, by simp, locallyLinear_bot⟩

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