ringConGen_mono — Mathlib

English

If r ⊆ s, then ringConGen r ≤ ringConGen s.

Русский

Если r ⊆ s, тогда ringConGen(r) ≤ ringConGen(s).

LaTeX

$$$$ r \subseteq s \Rightarrow \operatorname{ringConGen}(r) \le \operatorname{ringConGen}(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`. -/
theorem ringConGen_mono {r s : R → R → Prop} (h : ∀ x y, r x y → s x y) : ringConGen r ≤ ringConGen s :=
  ringConGen_le fun x y hr => RingConGen.Rel.of _ _ <| h x y hr

Похожие утверждения