unop_closure — Mathlib

English

The unop map commutes with closure: the unop of the closure in the opposite is the closure of the preimage under op.

Русский

unop commute с closure: (closure S).unop = closure (MulOpposite.op ⁻¹' S).

LaTeX

$$$(closure S).unop = closure (MulOpposite.op^{-1} S)$$$

Lean4

@[to_additive]
theorem unop_closure (s : Set Gᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s) :=
  by
  rw [← op_inj, op_unop, op_closure]
  simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

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