op_closure — Mathlib

English

The opposite of the closure of a set s is the closure of its image under unop: closure(s)^{op} = closure(preimage unop s).

Русский

Противоположность замыкания множества равно замыканию образа обратного изображения.

LaTeX

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

Lean4

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

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