iUnion_diff

Mathlib.Data.Set.Lattice

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

English

The difference between a set s and the union of a family t_i equals the union of differences: (⋃_i t_i) \ s = ⋃_i (t_i \ s).

Русский

Разность ⋃_i t_i и s равна ⋃_i (t_i \ s).

LaTeX

$$$ (\bigcup_i t_i) \setminus s = \bigcup_i (t_i \setminus s) $$$

Lean4

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

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

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

Разделы

Аффилиация

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