English
The infimum of a set of RingCon relations, when viewed as Setoid relations, coincides with the infimum of their images under toSetoid.
Русский
Наименьшее отношение конгруэнций RingCon совпадает с наименьшим отношением, полученным при переводе в соответствующее отношение эквивалентности.
LaTeX
$$$$ (\\mathrm{sInf}\, S)^{\\sim} = \\mathrm{sInf}\\bigl(\\{ r^{\\sim} : r \\in S \\} \\bigr) $$$$
Lean4
/-- The infimum of a set of congruence relations is the same as the infimum of the set's image
under the map to the underlying equivalence relation. -/
theorem sInf_toSetoid (S : Set (RingCon R)) : (sInf S).toSetoid = sInf ((·.toSetoid) '' S) :=
Setoid.ext fun x y => ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩
