# Theory Nash_Extras

```section ‹The Pointwise Less-Than Relation Between Two Sets›

theory Nash_Extras
imports "HOL-Library.Ramsey" "HOL-Library.Countable_Set"

begin

definition less_sets :: "['a::order set, 'a::order set] ⇒ bool" (infixr "≪" 50)
where "A ≪ B ≡ ∀x∈A. ∀y∈B. x < y"

lemma less_sets_empty[iff]: "S ≪ {}" "{} ≪ T"
by (auto simp: less_sets_def)

lemma less_setsD: "⟦A ≪ B; a ∈ A; b ∈ B⟧ ⟹ a < b"
by (auto simp: less_sets_def)

lemma less_sets_irrefl [simp]: "A ≪ A ⟷ A = {}"
by (auto simp: less_sets_def)

lemma less_sets_trans: "⟦A ≪ B; B ≪ C; B ≠ {}⟧ ⟹ A ≪ C"
unfolding less_sets_def using less_trans by blast

lemma less_sets_weaken1: "⟦A' ≪ B; A ⊆ A'⟧ ⟹ A ≪ B"
by (auto simp: less_sets_def)

lemma less_sets_weaken2: "⟦A ≪ B'; B ⊆ B'⟧ ⟹ A ≪ B"
by (auto simp: less_sets_def)

lemma less_sets_imp_disjnt: "A ≪ B ⟹ disjnt A B"
by (auto simp: less_sets_def disjnt_def)

lemma less_sets_UN1: "less_sets (⋃𝒜) B ⟷ (∀A∈𝒜. A ≪ B)"
by (auto simp: less_sets_def)

lemma less_sets_UN2: "less_sets A (⋃ ℬ) ⟷ (∀B∈ℬ. A ≪ B)"
by (auto simp: less_sets_def)

lemma less_sets_Un1: "less_sets (A ∪ A') B ⟷ A ≪ B ∧ A' ≪ B"
by (auto simp: less_sets_def)

lemma less_sets_Un2: "less_sets A (B ∪ B') ⟷ A ≪ B ∧ A ≪ B'"
by (auto simp: less_sets_def)

lemma strict_sorted_imp_less_sets:
"strict_sorted (as @ bs) ⟹ (list.set as) ≪ (list.set bs)"