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 ι)
:
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 (i : ι) (h : i ∈ []) => nomatch (_ : False)⟧
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⟧