div_iUnion

Mathlib.Algebra.Group.Pointwise.Set.Lattice

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

English

Division distributes over a union indexed by i: s / ⋃ i, t_i = ⋃ i, s / t_i.

Русский

Деление по объединению, индексируемому i: s / ⋃ i, t_i = ⋃ i, s / t_i.

LaTeX

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

Lean4

@[to_additive]
theorem div_iUnion (s : Set α) (t : ι → Set α) : (s / ⋃ i, t i) = ⋃ i, s / t i :=
  image2_iUnion_right ..

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

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

Разделы

Аффилиация

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