singleton_op_unop — Mathlib

English

Let x be an element of α. The unop of the singleton {op x} in αᵒᵖ is the singleton {x} in α.

Русский

Пусть x ∈ α. Обратное к единичному множеству {op x} в αᵒᵖ равно единичному множеству {x} в α.

LaTeX

$$$ \operatorname{unop}(\{\operatorname{op}(x)\}) = \{x\}$$$

Lean4

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

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