op_closure — Mathlib

English

For any set s in M, the opposite of the closure of s equals the closure of the preimage of s under unop: (closure s).op = closure (unop^{-1} s).

Русский

Для множества s в M противоположность замыкания равна замыканию предварительного образа s под действием unop: (closure s).op = closure (unop^{-1} s).

LaTeX

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

Lean4

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

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