unop_le_unop_iff — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem unop_le_unop_iff {S₁ S₂ : Subgroup Gᵐᵒᵖ} : S₁.unop ≤ S₂.unop ↔ S₁ ≤ S₂ :=
  MulOpposite.unop_surjective.forall

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