op_iInf — Mathlib

English

The opposite of the infimum over a family of subsemirings is the infimum of the opposites: (iInf S).op = ⨅ i, (S i).op.

Русский

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

LaTeX

$$$ (\\mathrm{iInf} S)^{op} = \\bigwedge_i (S(i))^{op}$$$

Lean4

theorem op_iInf (S : ι → Subsemiring R) : (iInf S).op = ⨅ i, (S i).op :=
  opEquiv.map_iInf _

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