union_iInter

Mathlib.Data.Set.Lattice

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

English

Let s_i be sets and t be a fixed set. Then (⋃_{i} s_i) ∩ t = ⋂_{i} (s_i ∩ t).

Русский

Пусть для всех i множества s_i и фиксированное множество t. Тогда (⋃_{i} s_i) ∩ t = ⋂_{i} (s_i ∩ t).

LaTeX

$$$ \Big(\bigcup_i s_i\Big) \cap t = \bigcap_i (s_i \cap t) $$$

Lean4

theorem union_iInter (s : Set β) (t : ι → Set β) : (s ∪ ⋂ i, t i) = ⋂ i, s ∪ t i :=
  sup_iInf_eq _ _

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

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

Разделы

Аффилиация

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