op_sSup — Mathlib

English

The opposite of the supremum of a set of subsemirings is the supremum of the preimage under unop: (sSup S).op = sSup (preimage unop S).

Русский

Противоположность наибольшего элемента множества подполей равна наибольшему элементу их предобраза по unop.

LaTeX

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

Lean4

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

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