Ramsey arrow

Conjectura.Defs.Mathematics.Combinatorics.GraphTheory.RamseyArrow

/-
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
-/
import Mathlib.Data.Finset.Card

/-! # Ramsey arrow -/

namespace Conjectura.GraphTheory

/-- 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)

end Conjectura.GraphTheory