nonempty_of_union_eq_top_of_nonempty

English

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

Русский

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

LaTeX

$$$(\\\\bigcup_i s_i).Nonempty \\Rightarrow Nonempty\\, ι$$$

Lean4

theorem nonempty_of_union_eq_top_of_nonempty {ι : Type*} (t : Set ι) (s : ι → Set α) (H : Nonempty α)
    (w : ⋃ i ∈ t, s i = ⊤) : t.Nonempty :=
  by
  obtain ⟨x, m, -⟩ := exists_set_mem_of_union_eq_top t s w H.some
  exact ⟨x, m⟩

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