op_closure — Mathlib

English

Let s be a subset of R. The opposite of the closure of s equals the closure of the preimage of s under unop: (closure s).op = closure (MulOpposite.unop ⁻¹' s).

Русский

Пусть s — множество в R. Противоположность замыкания s равна замыканию множества, полученного через предобразие по unop: (closure s).op = closure (MulOpposite.unop ⁻¹' s).

LaTeX

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

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

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