inter_setOf_eq_sep — Mathlib

English

The intersection of a set with a setOf predicate equals the setOf elements of the set satisfying the predicate.

Русский

Пересечение множества с множеством, задаваемым предикатом, равно множеству элементов множества, удовлетворяющих предикату.

LaTeX

$$\{a \mid p\,a\} \cap s = {a \in s \mid p\,a}$$

Lean4

theorem inter_setOf_eq_sep (s : Set α) (p : α → Prop) : s ∩ {a | p a} = {a ∈ s | p a} :=
  rfl

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