op_sSup

Mathlib.Algebra.Ring.Subring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subring.op_sSup

English

The op of the supremum of a set equals the supremum of the preimage under unop.

Русский

Образ op верхней границы множества равен верхней границе предобраза по unop.

LaTeX

$$$(\operatorname{sSup} S)^{op} = \operatorname{sSup}(\mathrm{unop}^{-1} S)$$$

Lean4

theorem op_sSup (S : Set (Subring R)) : (sSup S).op = sSup (.unop ⁻¹' S) :=
  opEquiv.map_sSup_eq_sSup_symm_preimage _

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

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

Разделы

Аффилиация

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