setOf_exists — Mathlib

English

The set of x for which there exists i with p(i, x) equals the union of the sets {x | p(i, x)} over i.

Русский

Множество всех x, для которых существует i с p(i, x), равно объединению множеств {x | p(i, x)} по i.

LaTeX

$${$\\{x \\mid \\exists i, p(i, x)\\}} = \\bigcup_i \\{x \\mid p(i, x)\\}$$$

Lean4

theorem setOf_exists (p : ι → β → Prop) : {x | ∃ i, p i x} = ⋃ i, {x | p i x} :=
  ext fun _ => mem_iUnion.symm

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