op_iSup — Mathlib

English

The opposite of the directed supremum over a family of subsemirings is the supremum of the opposites: (iSup S).op = ⨆ i, (S i).op.

Русский

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

LaTeX

$$$ (\\mathrm{iSup} S)^{op} = \\big\\lbrace \\,(S(i))^{op} \\,\\big\\rbrace_i $$$

Lean4

theorem op_iSup (S : ι → Subsemiring R) : (iSup S).op = ⨆ i, (S i).op :=
  opEquiv.map_iSup _

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