Mathlib.Data.Fintype.OfMap

Fintype.ofMultiset definition

[DecidableEq α] (s : Multiset α) (H : ∀ x : α, x ∈ s) : Fintype α

Full source

/-- Construct a proof of `Fintype α` from a universal multiset -/
def ofMultiset [DecidableEq α] (s : Multiset α) (H : ∀ x : α, x ∈ s) : Fintype α :=
  ⟨s.toFinset, by simpa using H⟩

Finite type from a universal multiset

Informal description

Given a multiset `s` of elements of type `α` (with decidable equality) such that every element of `α` appears in `s`, the type `α` is finite. The proof constructs a finite set (finset) from the multiset `s` and shows that it contains all elements of `α`.

Fintype.ofList definition

[DecidableEq α] (l : List α) (H : ∀ x : α, x ∈ l) : Fintype α

Full source

/-- Construct a proof of `Fintype α` from a universal list -/
def ofList [DecidableEq α] (l : List α) (H : ∀ x : α, x ∈ l) : Fintype α :=
  ⟨l.toFinset, by simpa using H⟩

Finite type from a universal list

Informal description

Given a list `l` of elements of type `α` (with decidable equality) such that every element of `α` appears in `l`, the type `α` is finite. The proof constructs a finite set (finset) from the list `l` and shows that it contains all elements of `α$.

Fintype.ofBijective definition

[Fintype α] (f : α → β) (H : Function.Bijective f) : Fintype β

Full source

/-- If `f : α → β` is a bijection and `α` is a fintype, then `β` is also a fintype. -/
def ofBijective [Fintype α] (f : α → β) (H : Function.Bijective f) : Fintype β :=
  ⟨univ.map ⟨f, H.1⟩, fun b =>
    let ⟨_, e⟩ := H.2 b
    e ▸ mem_map_of_mem _ (mem_univ _)⟩

Finite type via bijection

Informal description

Given a finite type $\alpha$ and a bijective function $f : \alpha \to \beta$, the type $\beta$ is also finite. The finite set for $\beta$ is constructed by applying $f$ to the universal finite set of $\alpha$.

Fintype.ofSurjective definition

[DecidableEq β] [Fintype α] (f : α → β) (H : Function.Surjective f) : Fintype β

Full source

/-- If `f : α → β` is a surjection and `α` is a fintype, then `β` is also a fintype. -/
def ofSurjective [DecidableEq β] [Fintype α] (f : α → β) (H : Function.Surjective f) : Fintype β :=
  ⟨univ.image f, fun b =>
    let ⟨_, e⟩ := H b
    e ▸ mem_image_of_mem _ (mem_univ _)⟩

Finite type via surjection

Informal description

Given a finite type $\alpha$ and a surjective function $f : \alpha \to \beta$ (with decidable equality on $\beta$), the type $\beta$ is also finite. The finite set for $\beta$ is constructed as the image of the universal finite set of $\alpha$ under $f$.

Fintype.ofInjective definition

[Fintype β] (f : α → β) (H : Function.Injective f) : Fintype α

Full source

/-- Given an injective function to a fintype, the domain is also a
fintype. This is noncomputable because injectivity alone cannot be
used to construct preimages. -/
noncomputable def ofInjective [Fintype β] (f : α → β) (H : Function.Injective f) : Fintype α :=
  letI := Classical.dec
  if hα : Nonempty α then
    letI := Classical.inhabited_of_nonempty hα
    ofSurjective (invFun f) (invFun_surjective H)
  else ⟨∅, fun x => (hα ⟨x⟩).elim⟩

Finite type via injection

Informal description

Given a finite type $\beta$ and an injective function $f : \alpha \to \beta$, the domain type $\alpha$ is also finite. The finite set for $\alpha$ is constructed using the inverse function of $f$ (which is surjective when $f$ is injective) applied to the universal finite set of $\beta$.

Fintype.ofEquiv definition

(α : Type*) [Fintype α] (f : α ≃ β) : Fintype β

Full source

/-- If `f : α ≃ β` and `α` is a fintype, then `β` is also a fintype. -/
def ofEquiv (α : Type*) [Fintype α] (f : α ≃ β) : Fintype β :=
  ofBijective _ f.bijective

Finite type via equivalence

Informal description

Given a finite type $\alpha$ and a type equivalence (bijection) $f : \alpha \simeq \beta$, the type $\beta$ is also finite. The finite set for $\beta$ is constructed by applying $f$ to the universal finite set of $\alpha$.

Fintype.ofSubsingleton definition

(a : α) [Subsingleton α] : Fintype α

Full source

/-- Any subsingleton type with a witness is a fintype (with one term). -/
def ofSubsingleton (a : α) [Subsingleton α] : Fintype α :=
  ⟨{a}, fun _ => Finset.mem_singleton.2 (Subsingleton.elim _ _)⟩

Finite type structure for subsingletons

Informal description

Given a type `α` that is a subsingleton (i.e., all elements are equal) and a witness `a : α`, the type `α` is finite, with the finite set containing only the element `a`.

Fintype.univ_ofSubsingleton theorem

(a : α) [Subsingleton α] : @univ _ (ofSubsingleton a) = { a }

Full source

theorem univ_ofSubsingleton (a : α) [Subsingleton α] : @univ _ (ofSubsingleton a) = {a} :=
  rfl

Universal Set of Subsingleton is Singleton

Informal description

For any subsingleton type $\alpha$ (where all elements are equal) with a witness element $a \in \alpha$, the universal finite set of $\alpha$ is exactly the singleton set $\{a\}$.

Fintype.ofIsEmpty definition

[IsEmpty α] : Fintype α

Full source

/-- An empty type is a fintype. Not registered as an instance, to make sure that there aren't two
conflicting `Fintype ι` instances around when casing over whether a fintype `ι` is empty or not. -/
def ofIsEmpty [IsEmpty α] : Fintype α :=
  ⟨∅, isEmptyElim⟩

Finite structure for empty types

Informal description

Given an empty type $\alpha$ (i.e., a type with no elements), the type $\alpha$ is finite, with the empty set as its finite set of elements.

Fintype.univ_ofIsEmpty theorem

[IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅

Full source

/-- Note: this lemma is specifically about `Fintype.ofIsEmpty`. For a statement about
arbitrary `Fintype` instances, use `Finset.univ_eq_empty`. -/
theorem univ_ofIsEmpty [IsEmpty α] : @univ α Fintype.ofIsEmpty = ∅ :=
  rfl

Universal Finite Set of Empty Type is Empty

Informal description

For any empty type $\alpha$, the universal finite set of $\alpha$ (constructed via `Fintype.ofIsEmpty`) is equal to the empty set $\emptyset$.

Fintype.instEmpty instance

: Fintype Empty

Full source

instance : Fintype Empty := Fintype.ofIsEmpty

Finiteness of the Empty Type

Informal description

The empty type is finite.

Fintype.instPEmpty instance

: Fintype PEmpty

Full source

instance : Fintype PEmpty := Fintype.ofIsEmpty

Finiteness of the Empty Type `PEmpty`

Informal description

The type `PEmpty` is finite.

Main results