unop_sSup — Mathlib

English

The unop of the supremum equals the supremum of the preimage under op: (sSup S).unop = sSup (preimage op S).

Русский

Обратная от наибольшего элемента равна наибольшему элементу предобраза по op.

LaTeX

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

Lean4

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

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