Documentation

Mathlib.Data.Fintype.Quotient

Quotients of families indexed by a finite type #

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

Main definitions #

def Quotient.finChoiceAux {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) :
((i : ι) → i lQuotient (S i))Quotient inferInstance

An auxiliary function for Quotient.finChoice. 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
  • One or more equations did not get rendered due to their size.
  • Quotient.finChoiceAux [] x_2 = fun (x : ι) (h : x []) => nomatch
Instances For
    theorem Quotient.finChoiceAux_eq {ι : Type u_1} [DecidableEq ι] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (l : List ι) (f : (i : ι) → i lα i) :
    (Quotient.finChoiceAux l fun (i : ι) (h : i l) => f i h) = f
    def Quotient.finChoice {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιType u_2} [S : (i : ι) → Setoid (α i)] (f : (i : ι) → Quotient (S i)) :
    Quotient inferInstance

    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
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem Quotient.finChoice_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιType u_2} [(i : ι) → Setoid (α i)] (f : (i : ι) → α i) :
      (Quotient.finChoice fun (i : ι) => f i) = f
      def Trunc.finChoice {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιType u_2} (f : (i : ι) → Trunc (α i)) :
      Trunc ((i : ι) → α i)

      Given a function that for each i : ι gives a term of the corresponding truncation type, then there is corresponding term in the truncation of the product.

      Equations
      Instances For
        theorem Trunc.finChoice_eq {ι : Type u_1} [DecidableEq ι] [Fintype ι] {α : ιType u_2} (f : (i : ι) → α i) :
        (Trunc.finChoice fun (i : ι) => Trunc.mk (f i)) = Trunc.mk f