English
A bijection between the indexed product of quotients and the quotient by the piSetoid on the family α i.
Русский
Биекция между произведением частиц Quotient и Quotient(piSetoid) для семейства α i.
LaTeX
$$$ (\forall i, \operatorname{Quotient}(r_i)) \simeq \operatorname{Quotient}(\pi\text{-Setoid}(r)) $$$
Lean4
/-- A bijection between an indexed product of quotients and the quotient by the product of the
equivalence relations. -/
@[simps]
noncomputable def piQuotientEquiv {ι : Sort*} {α : ι → Sort*} (r : ∀ i, Setoid (α i)) :
(∀ i, Quotient (r i)) ≃ Quotient (@piSetoid _ _ r)
where
toFun x := Quotient.mk'' fun i ↦ (x i).out
invFun
q :=
Quotient.liftOn' q (fun x i ↦ Quotient.mk'' (x i)) fun x y hxy ↦
by
ext i
simpa using hxy i
left_inv
q := by
ext i
simp
right_inv
q := by
refine Quotient.inductionOn' q fun _ ↦ ?_
simp only [Quotient.liftOn'_mk'', Quotient.eq'']
intro i
change Setoid.r _ _
rw [← Quotient.eq'']
simp
