iUnion_setOf — Mathlib

English

For a family of predicates P_i on α indexed by i, the union over i of the sets {x ∈ α | P_i(x)} equals the set {x ∈ α | ∃ i, P_i(x)}.

Русский

Пусть P_i — семейство предикатов на α. Тогда ⋃_i { x ∈ α | P_i(x) } = { x ∈ α | ∃ i, P_i(x) }.

LaTeX

$$$$ \\bigcup_{i} \\{ x \\in \\alpha \\mid P_i(x) \\} = \\{ x \\in \\alpha \\mid \\exists i,\\ P_i(x) \\} $$$$

Lean4

theorem iUnion_setOf (P : ι → α → Prop) : ⋃ i, {x : α | P i x} = {x : α | ∃ i, P i x} :=
  by
  ext
  exact mem_iUnion

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