singleton_eq_pair_iff

Mathlib.SetTheory.ZFC.Basic

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

← MathLib Explorer

English

For all x, y, z, {x} = {y, z} if and only if x = y and x = z.

Русский

Для всех x, y, z верно: {x} = {y, z} тогда и только тогда, когда x = y и x = z.

LaTeX

$$$ \{ x \} = \{ y, z \} \iff x = y \land x = z $$$

Lean4

@[simp]
theorem singleton_eq_pair_iff {x y z : ZFSet} : ({ x } : ZFSet) = { y, z } ↔ x = y ∧ x = z :=
  by
  rw [eq_comm, pair_eq_singleton_iff]
  simp_rw [eq_comm]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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