nonempty_of_nonempty_iUnion — Mathlib

English

If the union over i of s i equals the universal set, then ι is nonempty.

Русский

Если объединение по i множеств s(i) равно вселенной, тогда ι непусто.

LaTeX

$$$\\bigcup_i s_i = \\text{univ} \\Rightarrow Nonempty\\, ι$$$

Lean4

theorem nonempty_of_nonempty_iUnion {s : ι → Set α} (h_Union : (⋃ i, s i).Nonempty) : Nonempty ι :=
  by
  obtain ⟨x, hx⟩ := h_Union
  exact ⟨Classical.choose <| mem_iUnion.mp hx⟩

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