mem_def — Mathlib

English

For any a and any set s, the statement a ∈ s is equivalent to s a, i.e., membership equals application of the defining predicate.

Русский

Для любых a и множества s утверждение a ∈ s эквивалентно s(a), то есть принадлежность равна применению определяющего предиката.

LaTeX

$$$\forall {a} {s},\; a \in s \;\iff\; s(a)$$$

Lean4

@[deprecated "This lemma abuses the `Set α := α → Prop` defeq.
      If you think you need it you have already taken a wrong turn." (since := "2025-06-10")]
theorem mem_def {a : α} {s : Set α} : a ∈ s ↔ s a :=
  Iff.rfl

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