English
The join (supremum) of two congruences c and d is the smallest congruence containing the relation 'x is related to y by c or by d'.
Русский
Сумма (наименьшее верхнее значение) двух конгруэнций c и d есть наименьшая конгруэнция, содержащая отношение 'x связано с y через c или через d'.
LaTeX
$$$c \\sqcup d = conGen\\bigl(\\lambda x\\,y. c\\,x\,y \\lor d\\,x\,y\\bigr)$$$
Lean4
/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
the binary relation '`x` is related to `y` by `c` or `d`'. -/
@[to_additive sup_eq_addConGen /-- The supremum of additive congruence relations `c, d` equals the
smallest additive congruence relation containing the binary relation '`x` is related to `y`
by `c` or `d`'. -/
]
theorem sup_eq_conGen (c d : Con M) : c ⊔ d = conGen fun x y => c x y ∨ d x y :=
by
rw [conGen_eq]
apply congr_arg sInf
simp only [le_def, or_imp, ← forall_and]
