unop_sInf

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subsemiring.unop_sInf

English

The unop of the infimum equals the infimum of the preimage under op: (sInf S).unop = sInf (preimage op S).

Русский

Обратная от инфимина равна инфиму предобраза по op.

LaTeX

$$$ (\\mathrm{sInf} S)^{unop} = \\mathrm{sInf} (\\mathrm{preimage} \\mathrm{op} S) $$$

Lean4

theorem unop_sInf (S : Set (Subsemiring Rᵐᵒᵖ)) : (sInf S).unop = sInf (.op ⁻¹' S) :=
  opEquiv.symm.map_sInf_eq_sInf_symm_preimage _

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

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

Разделы

Аффилиация

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