unop_closure — Mathlib

English

For any s in M^{op}, (closure s).unop = closure (op^{-1} s).

Русский

Для множества s в M^{op}, (closure s).unop = closure (op^{-1} s).

LaTeX

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

Lean4

@[to_additive]
theorem unop_closure (s : Set Mᵐᵒᵖ) : (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']

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