mathlib3 documentation


Lemmas about finite and sets #

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