# Theory Nash_Extras

section ‹The Pointwise Less-Than Relation Between Two Sets›
theory Nash_Extras
imports "HOL-Library.Ramsey" "HOL-Library.Countable_Set"
begin
:: "['a::order set, 'a::order set] ⇒ bool" (infixr "≪" 50)
where "A ≪ B ≡ ∀x∈A. ∀y∈B. x < y"
lemma [iff]: "S ≪ {}" "{} ≪ T"
by (auto simp: less_sets_def)
lemma : "⟦A ≪ B; a ∈ A; b ∈ B⟧ ⟹ a < b"
by (auto simp: less_sets_def)
lemma [simp]: "A ≪ A ⟷ A = {}"
by (auto simp: less_sets_def)
lemma : "⟦A ≪ B; B ≪ C; B ≠ {}⟧ ⟹ A ≪ C"
unfolding less_sets_def using less_trans by blast
lemma : "⟦A' ≪ B; A ⊆ A'⟧ ⟹ A ≪ B"
by (auto simp: less_sets_def)
lemma : "⟦A ≪ B'; B ⊆ B'⟧ ⟹ A ≪ B"
by (auto simp: less_sets_def)
lemma : "A ≪ B ⟹ disjnt A B"
by (auto simp: less_sets_def disjnt_def)
lemma : "less_sets (⋃𝒜) B ⟷ (∀A∈𝒜. A ≪ B)"
by (auto simp: less_sets_def)
lemma : "less_sets A (⋃ ℬ) ⟷ (∀B∈ℬ. A ≪ B)"
by (auto simp: less_sets_def)
lemma : "less_sets (A ∪ A') B ⟷ A ≪ B ∧ A' ≪ B"
by (auto simp: less_sets_def)
lemma : "less_sets A (B ∪ B') ⟷ A ≪ B ∧ A ≪ B'"
by (auto simp: less_sets_def)
lemma :
"strict_sorted (as @ bs) ⟹ (list.set as) ≪ (list.set bs)"
by (simp add: less_sets_def sorted_wrt_append)
lemma :
fixes n::nat
assumes "Sup T < n" "finite T"
shows "less_sets T {n}"
using assms Max_less_iff
by (auto simp: Sup_nat_def less_sets_def split: if_split_asm)
end