Set is finite if image and fibers are finite?

Stream: Is there code for X?

[Michael Stoll]

Do we have something like the following?

lemma set.finite.of_finite_image_and_fibers {α β : Type*} (s : set α) (f : α → β) (h₁ : (f '' s).finite)
  (h₂ : ∀ b : β, (f ⁻¹' {b} ∩ s).finite) : s.finite

(This could also be an iff statement, I suppose.)
There is docs#set.finite.of_finite_image, but this requires the map to be injective.

[Michael Stoll]

Here is a proof.

lemma set.finite.of_finite_image_and_fibers {α β : Type*} (s : set α) (f : α → β) (h₁ : (f '' s).finite)
  (h₂ : ∀ b : β, (f ⁻¹' {b} ∩ s).finite) : s.finite :=
begin
  have H : s ⊆ ⋃ (b : β) (hb : b ∈ f '' s), (f ⁻¹' {b} ∩ s),
  { intros a ha,
    simp only [set.mem_image, set.Union_exists, set.bUnion_and', set.Union_Union_eq_right, set.mem_Union,
               set.mem_inter_iff, set.mem_preimage, set.mem_singleton_iff, exists_prop],
    exact ⟨a, ha, rfl, ha⟩, },
  exact set.finite.subset (set.finite.bUnion h₁ (λ b hb, h₂ b)) H,
end

[Michael Stoll]

And a similar kind of statement that might also be missing:

lemma infinite_iff_infinite {α β : Type*} {f : α → β} {s : set α} {t : set β} (h : bij_on f s t) :
  s.infinite ↔ t.infinite

[Matt Diamond]

infinite_iff_infinite is close to docs#equiv.infinite_iff

[Matt Diamond]

if you use docs#set.bij_on.equiv and docs#set.infinite_coe_iff

[Michael Stoll]

OK, thanks. My proof was

begin
  rw [← not_iff_not, not_infinite, not_infinite],
  refine ⟨λ H, set.bij_on.image_eq h ▸ finite.image f H,
          λ H, finite.of_finite_image _ (bij_on.inj_on h)⟩,
  exact (set.bij_on.image_eq h).symm ▸ H,
end

but yours is a one-liner

(set.infinite_coe_iff.symm.trans $ equiv.infinite_iff (set.bij_on.equiv f h)).trans set.infinite_coe_iff

[Michael Stoll]

I somehow tried to avoid using subtypes...