mathlib3 documentation

data.fintype.quotient

Quotients of families indexed by a finite type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file provides quotient.fin_choice, a mechanism to go from a finite family of quotients to a quotient of finite families.

Main definitions #

def quotient.fin_choice_aux {ι : Type u_1} [decidable_eq ι] {α : ι Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) :
(Π (i : ι), i l quotient (S i)) quotient pi_setoid

An auxiliary function for quotient.fin_choice. Given a collection of setoids indexed by a type ι, a (finite) list l of indices, and a function that for each i ∈ l gives a term of the corresponding quotient type, then there is a corresponding term in the quotient of the product of the setoids indexed by l.

Equations
theorem quotient.fin_choice_aux_eq {ι : Type u_1} [decidable_eq ι] {α : ι Type u_2} [S : Π (i : ι), setoid (α i)] (l : list ι) (f : Π (i : ι), i l α i) :
quotient.fin_choice_aux l (λ (i : ι) (h : i l), f i h) = f
def quotient.fin_choice {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι Type u_2} [S : Π (i : ι), setoid (α i)] (f : Π (i : ι), quotient (S i)) :

Given a collection of setoids indexed by a fintype ι and a function that for each i : ι gives a term of the corresponding quotient type, then there is corresponding term in the quotient of the product of the setoids.

Equations
theorem quotient.fin_choice_eq {ι : Type u_1} [decidable_eq ι] [fintype ι] {α : ι Type u_2} [Π (i : ι), setoid (α i)] (f : Π (i : ι), α i) :
quotient.fin_choice (λ (i : ι), f i) = f