# 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.

source
instance Set.fintypeRange {α : Type u} {ι : Sort w} [DecidableEq α] (f : ι → α) [Fintype (PLift ι)] :
Fintype ↑(range f)
Equations

- Set.fintypeRange f = Fintype.ofFinset (Finset.image (f ∘ PLift.down) Finset.univ) ⋯

### 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.

source
instance Finite.Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] :
Finite ↑(Set.range f)
source
instance Finite.Set.finite_replacement {α : Type u} {β : Type v} [Finite α] (f : α → β) :
Finite ↑{x : β | ∃ (x_1 : α), f x_1 = x}

### 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.

source
theorem Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] :
(range f).Finite
source
theorem Set.Finite.dependent_image {α : Type u} {β : Type v} {s : Set α} (hs : s.Finite) (F : (i : α) → i ∈ s → β) :
{y : β | ∃ (x : α) (hx : x ∈ s), F x hx = y}.Finite