op_sup — Mathlib

English

Taking opposite preserves the join of two subgroups: the opposite of the join is the join of the opposites.

Русский

Преобразование к противоположной группе сохраняет объединение двух подпгрупп: (S1 ⊔ S2)^{op} = S1^{op} ⊔ S2^{op}.

LaTeX

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

Lean4

@[to_additive]
theorem op_sup (S₁ S₂ : Subgroup G) : (S₁ ⊔ S₂).op = S₁.op ⊔ S₂.op :=
  opEquiv.map_sup _ _

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