setOf_eq_eq_singleton'

Mathlib.Data.Set.Insert

URI: https://scilib.ai/kg/mathlib#Set.setOf_eq_eq_singleton'

English

The set {x | a = x} is equal to {a}.

Русский

Множество {x | a = x} равно {a}.

LaTeX

$$$\\{ x \\mid a = x \\} = \\{ a \\}$$$

Lean4

@[simp]
theorem setOf_eq_eq_singleton' {a : α} : {x | a = x} = { a } :=
  ext fun _ => eq_comm

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

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

Разделы

Аффилиация

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