English
The supremum of a set S of equivalence relations is the equivalence closure of the binary relation 'there exists r ∈ S with x related to y by r'.
Русский
Супремум множества S отношений эквивалентности — это эквивгенционная замкнутость бинарного отношения 'существует r ∈ S такое, что x связано с y через r'.
LaTeX
$$$$ \\mathrm{sSup} S = \\mathrm{EqvGen.setoid}(\\lambda x y. \\exists r:\\ Setoid\\ α, r \\in S \\land r x y). $$$$
Lean4
/-- The supremum of a set S of equivalence relations is the equivalence closure of the binary
relation `there exists r ∈ S relating x and y`. -/
theorem sSup_eq_eqvGen (S : Set (Setoid α)) : sSup S = EqvGen.setoid fun x y => ∃ r : Setoid α, r ∈ S ∧ r x y :=
by
rw [eqvGen_eq]
apply congr_arg sInf
simp only [upperBounds, le_def, and_imp, exists_imp]
ext
exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩
