Documentation

Mathlib.Data.Finite.Set

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)] :