op_inf

Mathlib.Algebra.Ring.Subring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subring.op_inf

English

The op of the meet (infimum) equals the meet of the ops.

Русский

Образ op от пересечения равен пересечению образов.

LaTeX

$$$(S_1 \sqcap S_2)^{op} = S_1^{op} \sqcap S_2^{op}$$$

Lean4

theorem op_inf (S₁ S₂ : Subring R) : (S₁ ⊓ S₂).op = S₁.op ⊓ S₂.op :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru