English
For any set s of α × β, the finiteness of the images under fst and snd is equivalent to the finiteness of s itself.
Русский
Для множества s ⊆ α × β конечность образов fst(s) и snd(s) эквивалентна конечности самого s.
LaTeX
$$$ (\mathrm{image} \mathrm{fst} \ s).Finite \land (\mathrm{image} \mathrm{snd} \ s).Finite \iff s.Finite $$$
Lean4
theorem finite_image_fst_and_snd_iff {s : Set (α × β)} : (Prod.fst '' s).Finite ∧ (Prod.snd '' s).Finite ↔ s.Finite :=
⟨fun h => (h.1.prod h.2).subset fun _ h => ⟨mem_image_of_mem _ h, mem_image_of_mem _ h⟩, fun h =>
⟨h.image _, h.image _⟩⟩