English
The supremum of two equivalence relations r and s is the equivalence closure of the relation 'x is related to y by r or s'.
Русский
supremum двух отношений эквивалентности r и s равен замыканию по эквивалентности бинарному отношению ‘x связан с y по r или по s’.
LaTeX
$$$$ r \\oplus s = \\mathrm{EqvGen.setoid}(\\lambda x y. r\\ x\\ y \\lor s\\ x\\ y). $$$$
Lean4
/-- The supremum of two equivalence relations r and s is the equivalence closure of the binary
relation `x is related to y by r or s`. -/
theorem sup_eq_eqvGen (r s : Setoid α) : r ⊔ s = EqvGen.setoid fun x y => r x y ∨ s x y :=
by
rw [eqvGen_eq]
apply congr_arg sInf
simp only [le_def, or_imp, ← forall_and]
