setOf_mem_eq

Mathlib.Data.Set.Operations

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

English

The set { x | x ∈ s } is equal to s.

Русский

Множество { x | x ∈ s } равно множеству s.

LaTeX

$$$\\{ x \\mid x \\in s \\} = s$$$

Lean4

@[simp]
theorem setOf_mem_eq {s : Set α} : {x | x ∈ s} = s :=
  rfl

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

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

Разделы

Аффилиация

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