ringConGen_le — Mathlib

English

If r(x,y) implies c(x,y) for all x,y, then ringConGen r ≤ c.

Русский

Если r(x,y) ⇒ c(x,y) для всех x,y, то ringConGen(r) ≤ c.

LaTeX

$$$$ \forall x,y, r(x,y) \Rightarrow c(x,y) \implies \operatorname{ringConGen}(r) \le c $$$$

Lean4

/-- The smallest congruence relation containing a binary relation `r` is contained in any
congruence relation containing `r`. -/
theorem ringConGen_le {r : R → R → Prop} {c : RingCon R} (h : ∀ x y, r x y → c x y) : ringConGen r ≤ c := by
  rw [ringConGen_eq]; exact sInf_le h

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