nonempty_biUnion — Mathlib

English

For a family of sets {s_i} indexed by i in a set t, the union ⋃ i ∈ t, s_i is nonempty if and only if there exists i ∈ t with s_i nonempty.

Русский

Для семейства множеств {s_i}, индексированного i∈t, объединение ⋃ i∈t, s_i непусто тогда, когда существует i∈t такое, что s_i непусто.

LaTeX

$$$$\\left(\\bigcup_{i \\in t} s_i\\right) \\neq \\emptyset \\;\\iff\\; \\exists i \\in t, \\; s_i \\neq \\emptyset$$$$

Lean4

theorem nonempty_biUnion {t : Set α} {s : α → Set β} : (⋃ i ∈ t, s i).Nonempty ↔ ∃ i ∈ t, (s i).Nonempty := by simp

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