Lemmas about `finite` and `set`s #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we prove two lemmas about finite and sets.

Tags #

finiteness, finite sets

theorem finite.set.finite_of_finite_image {α : Type u} {β : Type v} (s : set α) {f : α → β} (h : set.inj_on f s) [finite ↥(f '' s)] :

theorem finite.of_injective_finite_range {α : Type u} {ι : Sort w} {f : ι → α} (hf : function.injective f) [finite ↥(set.range f)] :