of_sUnion_eq_univ — Mathlib

English

Let α be a nonempty type and s a collection of subsets of α. If the union of all members of s equals α, then the collection s is nonempty (i.e., contains at least one member).

Русский

Пусть α — непустое множество, и S — семейство подмножеств α. Если объединение всех элементов S равно α, то S непусто (существует как минимум один элемент).

LaTeX

$$$$ \\alpha \\neq \\varnothing \\quad \\land \\quad \\bigcup s = \\alpha \\quad \\Longrightarrow \\quad \\exists A \\in s.$$$$

Lean4

theorem of_sUnion_eq_univ [Nonempty α] {s : Set (Set α)} (h : ⋃₀ s = univ) : s.Nonempty :=
  Nonempty.of_sUnion <| h.symm ▸ univ_nonempty

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