singleton_unop — Mathlib

English

The unop of a singleton in αᵒᵖ is the singleton of the unop of its element.

Русский

Обратная операция unop для множества-единички в αᵒᵖ даёт единственное множество, содержащее unop элемента.

LaTeX

$$({x}: Set α^{\mathrm{op}}).unop = {\mathrm{unop} x}$$

Lean4

@[simp]
theorem singleton_unop (x : αᵒᵖ) : ({ x } : Set αᵒᵖ).unop = {unop x} :=
  by
  ext
  constructor
  · apply op_injective
  · apply unop_injective

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