iUnion_inter

Mathlib.Data.Set.Lattice

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

English

The union distributes over intersection: (⋃ i t_i) ∩ s = ⋃ i (t_i ∩ s).

Русский

Объединение распределяется по пересечению: (⋃ i t_i) ∩ s = ⋃ i (t_i ∩ s).

LaTeX

$$$$ \\left( \\bigcup_{i} t_i \\right) \\cap s = \\bigcup_{i} (t_i \\cap s) $$$$

Lean4

theorem iUnion_inter (s : Set β) (t : ι → Set β) : (⋃ i, t i) ∩ s = ⋃ i, t i ∩ s :=
  iSup_inf_eq _ _

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

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

Разделы

Аффилиация

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