English
The product of two Setoids r on α and s on β yields a Setoid on α × β where (a,b) is related to (a',b') iff a ~_r a' and b ~_s b'.
Русский
Произведение двух отношений: (a,b) связано с (a',b') тогда и только тогда a ~_r a' и b ~_s b'.
LaTeX
$$$ (r \mathrm{.prod} s).r ( (a,b) ) ( (a',b') ) \iff r(a,a') \land s(b,b') $$$
Lean4
/-- Given types `α`, `β`, the product of two equivalence relations `r` on `α` and `s` on `β`:
`(x₁, x₂), (y₁, y₂) ∈ α × β` are related by `r.prod s` iff `x₁` is related to `y₁`
by `r` and `x₂` is related to `y₂` by `s`. -/
protected def prod (r : Setoid α) (s : Setoid β) : Setoid (α × β)
where
r x y := r x.1 y.1 ∧ s x.2 y.2
iseqv :=
⟨fun x => ⟨r.refl' x.1, s.refl' x.2⟩, fun h => ⟨r.symm' h.1, s.symm' h.2⟩, fun h₁ h₂ =>
⟨r.trans' h₁.1 h₂.1, s.trans' h₁.2 h₂.2⟩⟩
