op_closure — Mathlib

English

Taking opposites commutes with subgroup closure: the opposite of the closure of a set equals the closure of the opposite preimage.

Русский

Противоположная операция и замыкание множеств коммутируют: (closure S)^{op} = closure (MulOpposite.unop ⁻¹' S).

LaTeX

$$$\mathrm{op\_closure}(s) : (closure\ s)^{op} = closure\ (MulOpposite.unop^{-1}\ s)$$$

Lean4

@[to_additive]
theorem op_closure (s : Set G) : (closure s).op = closure (MulOpposite.unop ⁻¹' s) :=
  by
  simp_rw [closure, op_sInf, Set.preimage_setOf_eq, Subgroup.coe_unop]
  congr with a
  exact MulOpposite.unop_surjective.forall

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