iInter_subset_iUnion

Mathlib.Data.Set.Lattice

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

English

If the index set is nonempty, then ⋂_i s_i ⊆ ⋃_i s_i.

Русский

Пусть множество индексов непусто; тогда ⋂_i s_i ⊆ ⋃_i s_i.

LaTeX

$$$\bigcap_i s_i \subseteq \bigcup_i s_i$$$

Lean4

theorem iInter_subset_iUnion [Nonempty ι] {s : ι → Set α} : ⋂ i, s i ⊆ ⋃ i, s i :=
  iInf_le_iSup

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

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

Разделы

Аффилиация

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