nonempty_sUnion

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.nonempty_sUnion

English

The union over S is nonempty iff there exists some s ∈ S that is nonempty.

Русский

Объединение над S непусто тогда и только тогда, когда существует s ∈ S такое, что s непусто.

LaTeX

$$$ (\bigcup_0 S).Nonempty \iff \exists s \in S, s.Nonempty $$$

Lean4

@[simp]
theorem nonempty_sUnion {S : Set (Set α)} : (⋃₀ S).Nonempty ↔ ∃ s ∈ S, Set.Nonempty s := by simp [nonempty_iff_ne_empty]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru