mem_op

Mathlib.Algebra.Group.Subgroup.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subgroup.mem_op

English

For any x ∈ G^{op} and any Subgroup S ≤ G, x ∈ S^{op} if and only if unop(x) ∈ S.

Русский

Пусть x ∈ G^{op} и S ≤ G. Тогда x ∈ S^{op} тогда и только тогда, когда unop(x) ∈ S.

LaTeX

$$$x \in S^{\mathrm{op}} \iff \mathrm{unop}(x) \in S$$$

Lean4

@[to_additive (attr := simp)]
theorem mem_op {x : Gᵐᵒᵖ} {S : Subgroup G} : x ∈ S.op ↔ x.unop ∈ S :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru