mem_closure_inv

Mathlib.Algebra.Group.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#Submonoid.mem_closure_inv

English

For a set s in a group, x ∈ closure(s⁻¹) if and only if x⁻¹ ∈ closure(s).

Русский

Для множества s в группе: x ∈ closure(s⁻¹) тогда и только тогда, когда x⁻¹ ∈ closure(s).

LaTeX

$$x ∈ closure(s)^{-1} \\iff x^{-1} ∈ closure(s)$$

Lean4

@[to_additive]
theorem mem_closure_inv (s : Set G) (x : G) : x ∈ closure s⁻¹ ↔ x⁻¹ ∈ closure s := by rw [closure_inv, mem_inv]

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

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

Разделы

Аффилиация

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