English
The supremum over a set S of RingCon relations equals the smallest congruence containing the binary relation, where the relation is defined via existence in S.
Русский
Супремум множества конгруэнций S равен наименьшему конгруентному отношению, содержащему бинарное отношение, заданное через существование в S.
LaTeX
$$$$ \operatorname{sSup} S = \operatorname{ringConGen}( \lambda x y. \exists c \in S, c(x,y) ) $$$$
Lean4
/-- The supremum of a set of congruence relations `S` equals the smallest congruence relation
containing the binary relation 'there exists `c ∈ S` such that `x` is related to `y` by `c`'. -/
theorem sSup_eq_ringConGen (S : Set (RingCon R)) : sSup S = ringConGen fun x y => ∃ c : RingCon R, c ∈ S ∧ c x y :=
by
rw [ringConGen_eq]
apply congr_arg sInf
ext
exact ⟨fun h _ _ ⟨r, hr⟩ => h hr.1 hr.2, fun h r hS _ _ hr => h _ _ ⟨r, hS, hr⟩⟩
