Theory More_Set

(* ---------------------------------------------------------------------------- *)
subsection ‹Library Aditions for Set Cardinality›
(* ---------------------------------------------------------------------------- *)

text ‹In this section some additional simple lemmas about set cardinality are proved.›

theory More_Set
imports Main
begin

text ‹Every infinite set has at least two different elements›
lemma infinite_contains_2_elems:
  assumes "infinite A"
  shows "∃ x y. x ≠ y ∧ x ∈ A ∧ y ∈ A"
  by (metis assms finite.simps is_singletonI' is_singleton_def)

text ‹Every infinite set has at least three different elements›
lemma infinite_contains_3_elems:
  assumes "infinite A"
  shows "∃ x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A"
  by (metis Diff_iff assms infinite_contains_2_elems infinite_remove insertI1)

text ‹Every set with cardinality greater than 1 has at least two different elements›
lemma card_geq_2_iff_contains_2_elems:
  shows "card A ≥ 2 ⟷ finite A ∧ (∃ x y. x ≠ y ∧ x ∈ A ∧ y ∈ A)"
proof (intro iffI conjI)
  assume *: "finite A ∧ (∃ x y. x ≠ y ∧ x ∈ A ∧ y ∈ A)"
  thus "card A ≥ 2"
    by (metis card_0_eq card_Suc_eq empty_iff leI less_2_cases singletonD)
next
  assume *: "2 ≤ card A"
  then show "finite A"
    using card.infinite by force
  show "∃ x y. x ≠ y ∧ x ∈ A ∧ y ∈ A"
    by (meson "*" card_2_iff' in_mono obtain_subset_with_card_n)
qed

text ‹Set cardinality is at least 3 if and only if it contains three different elements›
lemma card_geq_3_iff_contains_3_elems:
  shows "card A ≥ 3 ⟷ finite A ∧ (∃ x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A)"
proof (intro iffI conjI)
  assume *: "card A ≥ 3"
  then show "finite A"
    using card.infinite by force
  show "∃ x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A"
    by (smt (verit, best) "*" card_2_iff' card_geq_2_iff_contains_2_elems le_cases3 not_less_eq_eq numeral_2_eq_2 numeral_3_eq_3)
next
  assume *: "finite A ∧ (∃ x y z. x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ x ∈ A ∧ y ∈ A ∧ z ∈ A)"
  thus "card A ≥ 3"
    by (metis One_nat_def Suc_le_eq card_2_iff' card_le_Suc0_iff_eq leI numeral_3_eq_3 one_add_one order_class.order.eq_iff plus_1_eq_Suc)
qed

text ‹Set cardinality of A is equal to 2 if and only if A={x, y} for two different elements x and y›
lemma card_eq_2_iff_doubleton: "card A = 2 ⟷ (∃ x y. x ≠ y ∧ A = {x, y})"
  using card_geq_2_iff_contains_2_elems[of A]
  using card_geq_3_iff_contains_3_elems[of A]
  by auto (rule_tac x=x in exI, rule_tac x=y in exI, auto)

lemma card_eq_2_doubleton:
  assumes "card A = 2" and "x ≠ y" and "x ∈ A" and "y ∈ A"
  shows "A = {x, y}"
  using assms card_eq_2_iff_doubleton[of A]
  by auto

text ‹Bijections map singleton to singleton sets›

lemma bij_image_singleton:
  shows "⟦f ` A = {b}; f a = b; bij f⟧ ⟹ A = {a}"
  by (metis bij_betw_def image_empty image_insert inj_image_eq_iff)

end