unop_sSup

Mathlib.Algebra.Ring.Subring.MulOpposite

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

English

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

Русский

Unop от верхней границы равен верхней границе предобраза по op.

LaTeX

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

Lean4

theorem unop_sSup (S : Set (Subring Rᵐᵒᵖ)) : (sSup S).unop = sSup (.op ⁻¹' S) :=
  opEquiv.symm.map_sSup_eq_sSup_symm_preimage _

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

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

Разделы

Аффилиация

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