Set.Finite for a set defined by exists over a finite Set

Stream: Is there code for X?

[Ira Fesefeldt]

I am looking for a proof that if my set is defined by an existential quantifier over a finite set, the set itself is also finite. I.e. something like this:

import Mathlib

example (f : ℕ → ℤ) (s : Set ℕ) (h_finite : Set.Finite s) : Set.Finite {z | ∃ n ∈ s, f n = z} := by sorry

Does that exist?

[Kyle Miller]

Yes, that set is the same as f '' s, and so it's

example (f : ℕ → ℤ) (s : Set ℕ) (h_finite : Set.Finite s) :
    Set.Finite {z | ∃ n ∈ s, f n = z} :=
  Set.Finite.image f h_finite

[Ira Fesefeldt]

Ah! I didn't thought about that view. Thanks!

[Ira Fesefeldt]

A slightly related, but probably more difficult question, which appeared a bit later on the actual proof I am working on...
I need the following lemma:

import Mathlib

inductive Values where
  | some : ℤ → Values
  | none : Values
  | conflict : Values

abbrev partialMap := ℕ → Values


instance union : Union partialMap where
  union := fun f g n =>
  match f n with
  | Values.some a => match g n with
    | Values.some _ => Values.conflict
    | Values.none => Values.some a
    | Values.conflict => Values.conflict
  | Values.none => g n
  | Values.conflict => Values.conflict

example (f : partialMap) (h_finite : Set.Finite { n | f n ≠ Values.none}) : Set.Finite {g | ∃ g', g ∪ g' = f} := sorry

My current approach is to generate a finite Set (Nat x Bool) from { n | f n ≠ Values.none}, define a surjektion from that set to {g | ∃ g', g ∪ g' = f} (where the bool controls conflicts or no conflicts and natural numbers control whether the function is defined) and prove that the image of the Surjektion is a subset of my goal set. That seems to work out, feels however quite cumbersome.

Does someone know a better approach with the tools of Mathlib or is that a reasonable approach?