# Theory Ramsey

```
section "Ramsey's Theorem"

theory Ramsey
imports Main "HOL-Library.Infinite_Set" "HOL-Library.Ramsey"

begin

text ‹Please note: this entire development has been updated and incorporated into
@{theory "HOL-Library.Ramsey"}  above. Below, some of the results of the original development are
linked to their current versions elsewhere in the Isabelle libraries. ›

subsection "Library lemmas"

lemma infinite_inj_infinite_image: "infinite Z ⟹ inj_on f Z ⟹ infinite (f ` Z)"
using finite_imageD by blast

lemma infinite_dom_finite_rng: "[| infinite A; finite (f ` A) |] ==> ∃b ∈ f ` A. infinite {a : A. f a = b}"

lemma infinite_mem: "infinite X ⟹ ∃x. x ∈ X"
using finite_insert by fastforce

lemma not_empty_least: "(Y::nat set) ≠ {} ⟹ ∃m. m ∈ Y ∧ (∀m'. m' ∈ Y ⟶ m ≤ m')"
by (meson Inf_nat_def1 bdd_below_bot cInf_lower)

subsection "Dependent Choice Variant"

lemma dc:
assumes trans: "trans r"
and P0: "P x0"
and Pstep: "⋀x. P x ⟹ ∃y. P y ∧ (x, y) ∈ r"
obtains f :: "nat ⇒ 'a" where "⋀n. P (f n)" and "⋀n m. n < m ⟹ (f n, f m) ∈ r"
by (metis P0 Pstep dependent_choice local.trans)

subsection "Ramsey's theorem"

lemma ramsey: "∀(s::nat) (r::nat) (YY::'a set) (f::'a set ⇒ nat).
infinite YY
∧ (∀X. X ⊆ YY ∧ finite X ∧ card X = r ⟶ f X < s)
⟶ (∃Y' t'.
Y' ⊆ YY
∧ infinite Y'
∧ t' < s
∧ (∀X. X ⊆ Y' ∧ finite X ∧ card X = r ⟶ f X = t'))"
using Ramsey by fastforce

end
```