sup_eq_ringConGen — Mathlib

English

The supremum of congruences equals the smallest congruence containing the pointwise joined relations.

Русский

Супремум конгруэнций равен наименьшему конгруэнсу, содержащему точечно объединённые отношения.

LaTeX

$$$$ c \sqcup d = \operatorname{ringConGen}\bigl( x \mapsto c(x) \lor d(x) igr) $$$$

Lean4

/-- The supremum of congruence relations `c, d` equals the smallest congruence relation containing
the binary relation '`x` is related to `y` by `c` or `d`'. -/
theorem sup_eq_ringConGen (c d : RingCon R) : c ⊔ d = ringConGen fun x y => c x y ∨ d x y :=
  by
  rw [ringConGen_eq]
  apply congr_arg sInf
  simp only [le_def, or_imp, ← forall_and]

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