mem_setOf

Mathlib.Data.Set.Operations

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

English

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

Русский

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

LaTeX

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

Lean4

theorem mem_setOf {a : α} {p : α → Prop} : a ∈ {x | p x} ↔ p a :=
  Iff.rfl

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

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

Разделы

Аффилиация

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