sup_def — Mathlib

English

The supremum of two congruences equals the smallest congruence containing the supremum of their underlying relations.

Русский

Супремум двух конгруэнций равен наименьшему конгруентному отношению, содержащему супремум их оснований.

LaTeX

$$$$ c \sqcup d = \operatorname{ringConGen}( \uparrow c \; \lor \; \uparrow d ) $$$$

Lean4

/-- The supremum of two congruence relations equals the smallest congruence relation containing
the supremum of the underlying binary operations. -/
theorem sup_def {c d : RingCon R} : c ⊔ d = ringConGen (⇑c ⊔ ⇑d) := by rw [sup_eq_ringConGen]; rfl

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