English
If binary relations r and s satisfy r ⊆ s, then the smallest congruence containing r is contained in the smallest congruence containing s.
Русский
Если отношения r и s удовлетворяют r ⊆ s, то наименьшее конгруэнтное отношение, содержащее r, содержится в наименьшем конгруэнтном отношении, содержащее s.
LaTeX
$$$(\\forall a,b\\, (r(a,b) \\Rightarrow s(a,b))) \\Rightarrow conGen(r) \\le conGen(s)$$$
Lean4
/-- Given binary relations `r, s` with `r` contained in `s`, the smallest congruence relation
containing `s` contains the smallest congruence relation containing `r`. -/
@[to_additive addConGen_mono /-- Given binary relations `r, s` with `r` contained in `s`, the
smallest additive congruence relation containing `s` contains the smallest additive congruence
relation containing `r`. -/
]
theorem conGen_mono {r s : M → M → Prop} (h : ∀ x y, r x y → s x y) : conGen r ≤ conGen s :=
conGen_le fun x y hr => ConGen.Rel.of _ _ <| h x y hr
