Theory Infinite

theory Infinite
  imports Main
begin

class infinite =
  assumes infinite_UNIV: "infinite (UNIV :: 'a set)"
begin

lemma arb_element: "finite Y ⟹ ∃x :: 'a. x ∉ Y"
  using ex_new_if_finite infinite_UNIV
  by blast

lemma arb_finite_subset: "finite Y ⟹ ∃X :: 'a set. Y ∩ X = {} ∧ finite X ∧ n ≤ card X"
proof -
  assume fin: "finite Y"
  then obtain X where "X ⊆ UNIV - Y" "finite X" "n ≤ card X"
    using infinite_UNIV
    by (metis Compl_eq_Diff_UNIV finite_compl infinite_arbitrarily_large order_refl)
  then show ?thesis
    by auto
qed

lemma arb_countable_map: "finite Y ⟹ ∃f :: (nat ⇒ 'a). inj f ∧ range f ⊆ UNIV - Y"
  using infinite_UNIV
  by (auto simp: infinite_countable_subset)

end

instance nat :: infinite
  by standard auto

end