singleton_op

Mathlib.Data.Set.Opposite

URI: https://scilib.ai/kg/mathlib#Set.singleton_op

English

The image of a singleton under op equals the singleton of op of the element.

Русский

Образ единичного множества под op совпадает с единичным множеством op от элемента.

LaTeX

$$({x}:\!Set\!\{ x \})^{\mathrm{op}} = {\mathrm{op} x}$$

Lean4

@[simp]
theorem singleton_op (x : α) : ({ x } : Set α).op = {op x} :=
  by
  ext
  constructor
  · apply unop_injective
  · apply op_injective

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru