English
Let r be a binary relation on a multiplicative structure M. The smallest congruence containing r is contained in any congruence that already contains r.
Русский
Пусть r — бинарное отношение на полуприведённой структуре M. Наименьшее конгруэнтное отношение, содержащее r, содержится во всех конгруэнциях, которые уже содержат r.
LaTeX
$$$\\left(\\forall x,y\\, (r(x,y) \\to c(x,y))\\right) \\Rightarrow conGen(r) \\le c$$$
Lean4
/-- The smallest congruence relation containing a binary relation `r` is contained in any
congruence relation containing `r`. -/
@[to_additive addConGen_le /-- The smallest additive congruence relation containing a binary
relation `r` is contained in any additive congruence relation containing `r`. -/
]
theorem conGen_le {r : M → M → Prop} {c : Con M} (h : ∀ x y, r x y → c x y) : conGen r ≤ c := by rw [conGen_eq];
exact sInf_le h
