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 #
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
- quotient.fin_choice_aux (i :: l) f = (f i _).lift_on₂ (quotient.fin_choice_aux l (λ (j : ι) (h : j ∈ l), f j _)) (λ (a : α i) (l_1 : Π (i : ι), i ∈ l → α i), ⟦(λ (j : ι) (h : j ∈ i :: l), dite (j = i) (λ (e : j = i), _.mpr a) (λ (e : ¬j = i), l_1 j _))⟧) _
- quotient.fin_choice_aux list.nil f = ⟦(λ (i : ι), false.elim)⟧
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
- quotient.fin_choice f = quotient.lift_on (quotient.rec_on finset.univ.val (λ (l : list ι), quotient.fin_choice_aux l (λ (i : ι) (_x : i ∈ l), f i)) _) (λ (f : Π (i : ι), i ∈ finset.univ.val → α i), ⟦(λ (i : ι), f i _)⟧) quotient.fin_choice._proof_2