pair_eq_singleton

Mathlib.SetTheory.ZFC.Basic

URI: https://scilib.ai/kg/mathlib#ZFSet.pair_eq_singleton

English

The set {x, x} equals {x}.

Русский

Множество {x, x} равно {x}.

LaTeX

$$$\forall x : ZFSet, \{ x, x \} = (\{ x \} : ZFSet)$$$

Lean4

@[simp]
theorem pair_eq_singleton (x : ZFSet) : { x, x } = ({ x } : ZFSet) :=
  by
  ext
  simp

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

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

Разделы

Аффилиация

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