Ramsey arrow

ArrowsTodef

The Ramsey arrow n → (s, t): every two-colouring of the edges of the complete graph on n vertices contains either an s-set with all edges the first colour or a t-set with all edges the second. Ramsey's theorem says such an n always exists; the least one is the Ramsey number, and almost none are known.

def ArrowsTo (n s t : ℕ) : Prop :=
  ∀ c : Fin n → Fin n → Bool, (∀ x y, c x y = c y x) →
    (∃ S : Finset (Fin n), S.card = s ∧ ∀ x ∈ S, ∀ y ∈ S, x ≠ y → c x y = true) ∨
    (∃ T : Finset (Fin n), T.card = t ∧ ∀ x ∈ T, ∀ y ∈ T, x ≠ y → c x y = false)

Used by

Problem GT-002 — the Ramsey number R(5,5)

From Mathlib

Data.Finset.Card

import Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.RamseyArrow · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits