nonempty_of_nonempty_iUnion_eq_univ

Mathlib.Data.Set.Lattice

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

← MathLib Explorer

English

From a nonempty union of sets, deduce a nonempty index set.

Русский

Из непустого объединения множеств следует непустое множество индексов.

LaTeX

$$Nonempty ι$$

Lean4

theorem nonempty_of_nonempty_iUnion_eq_univ {s : ι → Set α} [Nonempty α] (h_Union : ⋃ i, s i = univ) : Nonempty ι :=
  nonempty_of_nonempty_iUnion (s := s) (by simpa only [h_Union] using univ_nonempty)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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