ruzsaSzemerediNumber_mono — Mathlib

English

The natural-number version of RS-number respects monotonicity under finite type relations.

Русский

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

LaTeX

$$$$ \\text{ruzsaSzemerediNumberNat}_n \\le \\text{ruzsaSzemerediNumberNat}_{m} \\text{ if } n \\le m. $$$$

Lean4

theorem ruzsaSzemerediNumber_mono (f : α ↪ β) : ruzsaSzemerediNumber α ≤ ruzsaSzemerediNumber β := by
  classical
  refine findGreatest_mono ?_ (choose_mono _ <| Fintype.card_le_of_embedding f)
  rintro n ⟨G, _, rfl, hG⟩
  refine ⟨G.map f, inferInstance, ?_, hG.map _⟩
  rw [← card_map ⟨map f, Finset.map_injective _⟩, ← cliqueFinset_map G f]
  decide

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