Mathlib.Data.Set.Finite.Range

Module docstring

{"# Finiteness of Set.range

Implementation notes

Each result in this file should come in three forms: a Fintype instance, a Finite instance and a Set.Finite constructor.

Tags

finite sets ","### Fintype instances

Every instance here should have a corresponding Set.Finite constructor in the next section. ","### Finite instances

There is seemingly some overlap between the following instances and the Fintype instances in Data.Set.Finite. While every Fintype instance gives a Finite instance, those instances that depend on Fintype or Decidable instances need an additional Finite instance to be able to generally apply.

Some set instances do not appear here since they are consequences of others, for example Subtype.Finite for subsets of a finite type. ","### Constructors for Set.Finite

Every constructor here should have a corresponding Fintype instance in the previous section (or in the Fintype module).

The implementation of these constructors ideally should be no more than Set.toFinite, after possibly setting up some Fintype and classical Decidable instances. "}

Set.fintypeRange instance

[DecidableEq α] (f : ι → α) [Fintype (PLift ι)] : Fintype (range f)

Full source

instance fintypeRange [DecidableEq α] (f : ι → α) [Fintype (PLift ι)] : Fintype (range f) :=
  Fintype.ofFinset (Finset.univ.image <| f ∘ PLift.down) <| by simp

Finiteness of the Range of a Function from a Finite Domain

Informal description

For any function $f : \iota \to \alpha$ where $\iota$ is finite (as witnessed by `Fintype (PLift ι)`) and $\alpha$ has decidable equality, the range of $f$ is finite.

Finite.Set.finite_range instance

(f : ι → α) [Finite ι] : Finite (range f)

Full source

instance finite_range (f : ι → α) [Finite ι] : Finite (range f) := by
  classical
  haveI := Fintype.ofFinite (PLift ι)
  infer_instance

Finiteness of the Range of a Function with Finite Domain

Informal description

For any function $f : \iota \to \alpha$ with a finite domain $\iota$, the range of $f$ is finite.

Finite.Set.finite_replacement instance

[Finite α] (f : α → β) : Finite {f x | x : α}

Full source

instance finite_replacement [Finite α] (f : α → β) :
    Finite {f x | x : α} :=
  Finite.Set.finite_range f

Finiteness of the Image of a Function on a Finite Domain

Informal description

For any finite type $\alpha$ and function $f \colon \alpha \to \beta$, the image $\{f(x) \mid x \in \alpha\}$ is finite.

Set.finite_range theorem

(f : ι → α) [Finite ι] : (range f).Finite

Full source

theorem finite_range (f : ι → α) [Finite ι] : (range f).Finite :=
  toFinite _

Finiteness of the Range of a Function with Finite Domain

Informal description

For any function $f \colon \iota \to \alpha$ with a finite domain $\iota$, the range of $f$ (i.e., the set $\{f(x) \mid x \in \iota\}$) is finite.

Set.Finite.dependent_image theorem

{s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) : {y : β | ∃ x hx, F x hx = y}.Finite

Full source

theorem Finite.dependent_image {s : Set α} (hs : s.Finite) (F : ∀ i ∈ s, β) :
    {y : β | ∃ x hx, F x hx = y}.Finite := by
  have := hs.to_subtype
  simpa [range] using finite_range fun x : s => F x x.2

Finiteness of the Dependent Image of a Function on a Finite Set

Informal description

For any finite set $s \subseteq \alpha$ and a dependent function $F \colon \Pi_{x \in s} \beta$, the image set $\{y \in \beta \mid \exists x \in s, \exists h_x \in x \in s, F(x, h_x) = y\}$ is finite.