op_le_iff — Mathlib

English

For Subgroups S1 of G and S2 of G^{op}, we have S1.op ≤ S2 if and only if S1 ≤ S2.unop.

Русский

Для подгрупп S1 ⊆ G и S2 ⊆ G^{op} выполняется S1^{op} ≤ S2 тогда и только тогда, когда S1 ≤ S2^{unop}.

LaTeX

$${S1 : Subgroup G} {S2 : Subgroup G^{op}}: S1^{op} \le S2 \iff S1 \le S2^{unop}$$

Lean4

@[to_additive]
theorem op_le_iff {S₁ : Subgroup G} {S₂ : Subgroup Gᵐᵒᵖ} : S₁.op ≤ S₂ ↔ S₁ ≤ S₂.unop :=
  MulOpposite.op_surjective.forall

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