closure_inv — Mathlib

English

For any group G and set s ⊆ G, the closure commutes with inversion: closure(s)⁻¹ = closure(s⁻¹).

Русский

Для группы G и множества s ⊆ G замыкание пропускает инверсию: closure(s)⁻¹ = closure(s⁻¹).

LaTeX

$$closure(s)^{-1} = closure(s^{-1})$$

Lean4

@[to_additive]
theorem closure_inv (s : Set G) : closure s⁻¹ = (closure s)⁻¹ :=
  by
  apply le_antisymm
  · rw [closure_le, coe_inv, ← Set.inv_subset, inv_inv]
    exact subset_closure
  · rw [inv_le, closure_le, coe_inv, ← Set.inv_subset]
    exact subset_closure

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