mem_setOf_eq

Mathlib.Data.Set.Operations

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

English

For any a ∈ α and predicate p: α → Prop, a ∈ { x | p x } iff p a.

Русский

Для любого a и предиката p, a принадлежит { x | p x } тогда и только тогда, когда p a истинно.

LaTeX

$$$x \\in \\{ y \\mid p(y) \\} \\iff p(x)$$$

Lean4

@[simp, mfld_simps]
theorem mem_setOf_eq {x : α} {p : α → Prop} : (x ∈ {y | p y}) = p x :=
  rfl

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

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

Разделы

Аффилиация

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