unop_adjoin — Mathlib

English

The unop of the algebra generated by a set equals the algebra generated by the preimage under op.

Русский

Unop порождающей алгебры множества равен алгебре, порожденной предобразом по opp.

LaTeX

$$$$(\\mathrm{Algebra.adjoin}_R s)^{unop} = \\mathrm{Algebra.adjoin}_R (\\mathrm{MulOpposite.op}^{-1} s)$$$$

Lean4

theorem unop_adjoin (s : Set Aᵐᵒᵖ) : (Algebra.adjoin R s).unop = Algebra.adjoin R (MulOpposite.op ⁻¹' s) :=
  by
  apply toSubsemiring_injective
  simp_rw [Algebra.adjoin, unop_toSubsemiring, Subsemiring.unop_closure, Set.preimage_union]
  congr with x
  simp

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