ruzsaSzemerediNumberNat — Mathlib

English

The nat-number RS-number is monotone with respect to finite type embeddings.

Русский

RS-число по Натуру монотонно растет при встраиваниях конечных типов.

LaTeX

$$$$ \\text{Monotone } \\ ruzsaSzemerediNumberNat. $$$$

Lean4

/-- The `n`-th **Ruzsa-Szemerédi number** is the maximum number of edges a locally linear graph on
`n` vertices can have.

In other words, `ruzsaSzemerediNumberNat n` is the maximum number of edges a graph on `n` vertices
can have such that each edge belongs to exactly one triangle. -/
noncomputable def ruzsaSzemerediNumberNat (n : ℕ) : ℕ :=
  ruzsaSzemerediNumber (Fin n)

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