English
Given a collection of setoids indexed by a finite type, there is a canonical quotient of the product that corresponds to taking quotients coordinatewise.
Русский
Дана совокупность множеств с эквививалентностями, индексируемых конечным типом; существует канонический фактор-объект произведения, соответствующий по координатам кватами.
LaTeX
$$$\\mathrm{finChoice} : (\\forall i, \\ Quotient(S_i)) \\to \\ Quotient(\\Pi i, α_i)$$$
Lean4
/-- 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.
See `Quotient.choice` for the noncomputable general version. -/
def finChoice (q : ∀ i, Quotient (S i)) : @Quotient (∀ i, α i) piSetoid :=
by
let e :=
Equiv.subtypeQuotientEquivQuotientSubtype (fun l : List ι ↦ ∀ i, i ∈ l) (fun s : Multiset ι ↦ ∀ i, i ∈ s)
(fun i ↦ Iff.rfl) (fun _ _ ↦ Iff.rfl) ⟨_, Finset.mem_univ⟩
refine e.liftOn (fun l ↦ (listChoice fun i _ ↦ q i).map (fun a i ↦ a i (l.2 i)) ?_) ?_
· exact fun _ _ h i ↦ h i _
intro _ _ _
refine ind_fintype_pi (fun a ↦ ?_) q
simp_rw [listChoice_mk, Quotient.map_mk]
