unop_sup — Mathlib

English

If S1 and S2 are subalgebras of the opposite algebra Aᵐᵒᵖ, then unop preserves joins: the unop of the join is the join of the unops.

Русский

Если S1 и S2 — подалгебры противоположной алгебры Aᵐᵒᵖ, то операция unop сохраняет соединение: unop(S1 ⊔ S2) = unop(S1) ⊔ unop(S2).

LaTeX

$$$$(S_1 \\sqcup S_2)^{unop} = S_1^{unop} \\sqcup S_2^{unop}$$$$

Lean4

theorem unop_sup (S₁ S₂ : Subalgebra R Aᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
  opEquiv.symm.map_sup _ _

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