eq_mem_setOf — Mathlib

English

The predicate p is equal to the predicate x ↦ x ∈ { a | p a }. In other words, p(x) holds exactly when x ∈ { a | p a }.

Русский

Предикат p равен предикату x ↦ x ∈ { a | p a }. Иными словами, p(x) истинно тогда и только тогда, когда x ∈ { a | p a }.

LaTeX

$$$\\forall x,\\ p(x) \\iff x \\in \\{ a \\mid p(a) \\}$$$

Lean4

/-- This lemma is intended for use with `rw` where a membership predicate is needed,
hence the explicit argument and the equality in the reverse direction from normal.
See also `Set.mem_setOf_eq` for the reverse direction applied to an argument. -/
theorem eq_mem_setOf (p : α → Prop) : p = (· ∈ {a | p a}) :=
  rfl

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