English
The supremum of two congruences equals the smallest congruence containing the pointwise supremum of their underlying relations.
Русский
Супремум двух конгруэнций равен наименьшей конгруэнции, содержащей поэлементное объединение их базовых отношений.
LaTeX
$$$c \\sqcup d = conGen( (\\uparrow c) \\sqcup (\\uparrow d) )$$$
Lean4
/-- The supremum of two congruence relations equals the smallest congruence relation containing
the supremum of the underlying binary operations. -/
@[to_additive /-- The supremum of two additive congruence relations equals the smallest additive
congruence relation containing the supremum of the underlying binary operations. -/
]
theorem sup_def {c d : Con M} : c ⊔ d = conGen (⇑c ⊔ ⇑d) := by rw [sup_eq_conGen]; rfl
