op_iInf — Mathlib

English

For a family S_i of subrings in R, the opposite of their infimum equals the infimum of the opposites: (iInf S).op = ⨅ i, (S i).op.

Русский

Для семейства подкольц S_i в кольце R противоположность их infimum равносильна инфимууму противоположностей: (iInf S).op = ⨅ i, (S i).op.

LaTeX

$$$(\inf_i S_i)^{\mathrm{op}} = \inf_i (S_i^{\mathrm{op}})$$$

Lean4

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

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