unop_sup — Mathlib

English

The opposite of the join of two subgroups equals the join of their opposites, taken in the opposite setting.

Русский

Объединение подпгрупп в противоположной структуре сохраняется под операцией unop: (S1 ⊔ S2).unop = S1.unop ⊔ S2.unop.

LaTeX

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

Lean4

@[to_additive]
theorem unop_sup (S₁ S₂ : Subgroup Gᵐᵒᵖ) : (S₁ ⊔ S₂).unop = S₁.unop ⊔ S₂.unop :=
  opEquiv.symm.map_sup _ _

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