English
A bijection between the indexed product of quotients and the quotient by the product of the corresponding Setoid relations.
Русский
Биекция между индексированным произведением частиц и делением по произведению соответствующих Setoid отношений.
LaTeX
$$$ \Big( \forall i, \operatorname{Quotient}(r_i) \Big) \simeq \operatorname{Quotient}( \lambda i. r_i )$$$
Lean4
/-- A bijection between the product of two quotients and the quotient by the product of the
equivalence relations. -/
@[simps]
def prodQuotientEquiv (r : Setoid α) (s : Setoid β) : Quotient r × Quotient s ≃ Quotient (r.prod s)
where
toFun
| (x, y) => Quotient.map₂ Prod.mk (fun _ _ hx _ _ hy ↦ ⟨hx, hy⟩) x y
invFun
q :=
Quotient.liftOn' q (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) fun x y hxy ↦
Prod.ext (by simpa using hxy.1) (by simpa using hxy.2)
left_inv
q := by
rcases q with ⟨qa, qb⟩
exact Quotient.inductionOn₂' qa qb fun _ _ ↦ rfl
right_inv
q := by
simp only
refine Quotient.inductionOn' q fun _ ↦ rfl
