unop_closure — Mathlib

English

The unop of the closure of s equals the closure of the preimage of s under op.

Русский

Обратная к замыканию множества равна замыканию предобраза по op.

LaTeX

$$$\\mathrm{closure}(s)^{unop} = \\mathrm{closure}(\\mathrm{preimage}(\\mathrm{op})\,s)$$$

Lean4

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

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