English
The underlying relation of sInf S equals the sInf of the underlying relations of S.
Русский
Основа отношения sInf S равна наименьшему отношению основных элементов множества S.
LaTeX
$$$$ \operatorname{coe}(\operatorname{sInf} S) = \operatorname{sInf}(\{ \operatorname{coe}(s) : s \in S \}) $$$$
Lean4
/-- The supremum of a set of congruence relations is the same as the smallest congruence relation
containing the supremum of the set's image under the map to the underlying binary relation. -/
theorem sSup_def {S : Set (RingCon R)} : sSup S = ringConGen (sSup (@Set.image (RingCon R) (R → R → Prop) (⇑) S)) :=
by
rw [sSup_eq_ringConGen, sSup_image]
congr with (x y)
simp only [iSup_apply, iSup_Prop_eq, exists_prop]
