English
The supremum of a set of congruences equals the generator applied to the supremum of their underlying relations.
Русский
Супремум множества конгруэнций равен конгенератору, применённому к супремуму их базовых отношений.
LaTeX
$$$\\mathrm{sSup} S = conGen( \\mathrm{sSup}( (\\uparrow) '' 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. -/
@[to_additive /-- The supremum of a set of additive congruence relations is the same as the smallest
additive congruence relation containing the supremum of the set's image under the map to the
underlying binary relation. -/
]
theorem sSup_def {S : Set (Con M)} : sSup S = conGen (sSup ((⇑) '' S)) :=
by
rw [sSup_eq_conGen, sSup_image]
congr with (x y)
simp only [iSup_apply, iSup_Prop_eq, exists_prop]
