Lemmas about Finite and Sets

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.InjOn f s) [Finite ↑(f '' s)] : Finite ↑s

theorem Finite.of_injective_finite_range {α : Type u} {ι : Sort w} {f : ι → α} (hf : Function.Injective f) [Finite ↑(Set.range f)] : Finite ι