op_top — Mathlib

English

Let G be a group. The largest subgroup ⊤, when viewed in the opposite structure, remains the largest: the opposite of ⊤ is ⊤.

Русский

Пусть G — группа. Наибольшая подпгруппа, рассмотренная во множестве противоположной группы, остаётся наибольшей: ⊤^{op} = ⊤.

LaTeX

$$$(\top)^{op} = \top$$$

Lean4

@[to_additive (attr := simp)]
theorem op_top : (⊤ : Subgroup G).op = ⊤ :=
  rfl

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