English
The supremum of a set S of congruences equals the smallest congruence containing the relation 'there exists c ∈ S with c related x and y'.
Русский
Супремум множества конгруэнций S равен наименьшей конгруэнции, содержащей отношение 'существует c ∈ S такое, что c связывает x и y'.
LaTeX
$$$\\mathrm{sSup} S = conGen\\bigl( \\lambda x\\,y. \\exists c \\in S, c\\,x\,y \\bigr)$$$
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`'. -/
@[to_additive sSup_eq_addConGen /-- The supremum of a set of additive congruence relations `S`
equals the smallest additive congruence relation containing the binary relation 'there exists
`c ∈ S` such that `x` is related to `y` by `c`'. -/
]
theorem sSup_eq_conGen (S : Set (Con M)) : sSup S = conGen fun x y => ∃ c : Con M, c ∈ S ∧ c x y :=
by
rw [conGen_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⟩⟩
