of_sUnion

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.Nonempty.of_sUnion

English

If the union over s is nonempty, then s is nonempty.

Русский

Если объединение над s непусто, то само s непусто.

LaTeX

$$$ (\bigcup_0 s).Nonempty \rightarrow s.Nonempty $$$

Lean4

theorem of_sUnion {s : Set (Set α)} (h : (⋃₀ s).Nonempty) : s.Nonempty :=
  let ⟨s, hs, _⟩ := nonempty_sUnion.1 h
  ⟨s, hs⟩

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

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

Разделы

Аффилиация

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