op_sup — Mathlib

English

The opposite of the join of two subsemirings is the join of their opposites: (S1 ⊔ S2).op = S1.op ⊔ S2.op.

Русский

Противоположность объединения двух подполемов равна объединению их противоположностей.

LaTeX

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

Lean4

theorem op_sup (S₁ S₂ : Subsemiring R) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
  opEquiv.map_sup _ _

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