le_op_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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