unop_sSup — Mathlib

English

Unop preserves sSup over sets in the opposite direction: (sSup S).unop = sSup (op⁻¹' S).

Русский

Unop сохраняет sSup над множествами в противоположном направлении: (sSup S).unop = sSup (op⁻¹' S).

LaTeX

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

Lean4

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

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