Mathlib.Data.Finite.Set

Module docstring

{"# Lemmas about Finite and Sets

In this file we prove two lemmas about Finite and Sets.

Tags

finiteness, finite sets "}

Finite.Set.finite_of_finite_image theorem

(s : Set α) {f : α → β} (h : s.InjOn f) [Finite (f '' s)] : Finite s

Full source

theorem Finite.Set.finite_of_finite_image (s : Set α) {f : α → β} (h : s.InjOn f)
    [Finite (f '' s)] : Finite s :=
  Finite.of_equiv _ (Equiv.ofBijective _ h.bijOn_image.bijective).symm

Finiteness of Preimage under Injective Function with Finite Image

Informal description

Let $s$ be a subset of a type $\alpha$ and $f : \alpha \to \beta$ be a function that is injective on $s$. If the image $f(s)$ is finite, then $s$ is finite.

Finite.of_injective_finite_range theorem

{f : ι → α} (hf : Function.Injective f) [Finite (range f)] : Finite ι

Full source

theorem Finite.of_injective_finite_range {f : ι → α} (hf : Function.Injective f)
    [Finite (range f)] : Finite ι :=
  Finite.of_injective (Set.rangeFactorization f) (hf.codRestrict _)

Finiteness of Domain via Injective Function with Finite Range

Informal description

Let $f : \iota \to \alpha$ be an injective function. If the range of $f$ is finite, then the domain $\iota$ is also finite.