iUnion_eq_univ_iff — Mathlib

English

For a family f : ι → Set α, the union over i of f(i) equals univ if and only if every element of α lies in some f(i): ⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i.

Русский

Для семейства f : ι → Set α общий союз по i даёт единицу, если и только если каждый элемент α лежит в некоторых f(i): ⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i.

LaTeX

$$$$ \\bigcup_{i} f(i) = \\text{univ} \\iff \\forall x, \\exists i, x \\in f(i). $$$$

Lean4

theorem iUnion_eq_univ_iff {f : ι → Set α} : ⋃ i, f i = univ ↔ ∀ x, ∃ i, x ∈ f i := by
  simp only [eq_univ_iff_forall, mem_iUnion]

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