Stream: Beginner Questions

Topic: Using surjection to prove finiteness

Yiming Xu (Nov 30 2024 at 08:57):

I want to prove finiteness using a surjection. i.e.
"if f is a surjection from A to B, where A:'a set, B:'b set, then if A is finite, then B is finite".

But there is no surj_on predicate, the only thing that I can find is about surjections on the universe. May I please ask if there exist any theorem I can appeal to?

Yiming Xu (Nov 30 2024 at 08:59):

Aha I find this...

Finite_Set.finite_vimageD': finite (?f -` ?A) ⟹ ?A ⊆ range ?f ⟹ finite ?A

Please let me know if it is not conventionally the best one for this case.

Yiming Xu (Nov 30 2024 at 09:07):

Oh it is not what I want because it requires the collection of elements of f(A), regardless whether it comes from A or not, is finite. I am still in trouble.

Yiming Xu (Nov 30 2024 at 09:28):

Okay... I can do:

lemma surj_on_finite_lemma:
  assumes "⋀b . b ∈ B  ⟹ ∃ a. a ∈ A ∧ f a = b"
     and "finite A"
   shows "finite B"
proof -
  obtain g where "⋀b. b ∈ B ⟹ g b ∈ A ∧ (f (g b)) = b"
    by (metis assms(1) f_inv_into_f imageI inv_into_into)
  then have "inj_on g B"
    by (metis  inj_on_inverseI)
  show ?thesis using finite_vimage_IntI[of A g B]

    by (simp add: Int_absorb2 ‹⋀b. b ∈ B ⟹ g b ∈ A ∧ f (g b) = b›
  ‹inj_on g B› assms(2) inf_commute subset_iff)
qed

But I am very surprised why it is already a lemma written there.

Balazs Toth (Nov 30 2024 at 09:31):

I also find it a pity that we don't have a surj_on predicate in the standard library. I defined my own definitions I work with:

abbreviation surj_on where
  "surj_on f domain ≡ (∀y. ∃x ∈ domain. y = f x)"

lemma surj_on_alternative: "surj_on f domain ⟷ f ` domain = UNIV"
  by auto

These work quite well with the lemmas I need.

For your exact problem, a lemma that will probably work for you is: Finite_Set.finite_surj

Yiming Xu (Nov 30 2024 at 09:40):

Aha this is what I want exactly!!! Thank you!

Last updated: Dec 21 2024 at 16:20 UTC