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.

instance Set.fintypeRange {α : Type u} {ι : Sort w} [DecidableEq α] (f : ι → α) [Fintype (PLift ι)] : Fintype ↑(Set.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.

instance Finite.Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] : Finite ↑(Set.range f)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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.

theorem Set.finite_range {α : Type u} {ι : Sort w} (f : ι → α) [Finite ι] : (Set.range f).Finite

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