unop_eq_top — Mathlib

English

Let S be a subgroup of the opposite group Gᵐᵒᵖ. Taking unop yields that S.unop equals ⊤ if and only if S equals ⊤.

Русский

Пусть S — подпгруппа G^{op}. Принятие обратного отображения даёт: S.unop = ⊤ ⇔ S = ⊤.

LaTeX

$$$S^{\mathrm{unop}} = \top \iff S = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem unop_eq_top {S : Subgroup Gᵐᵒᵖ} : S.unop = ⊤ ↔ S = ⊤ :=
  unop_injective.eq_iff' unop_top

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