iUnion_div — Mathlib

English

Division distributes over union: the quotient of a union of sets by t is equal to the union of quotients by t. Symbolically, (⋃ i, s_i) / t = ⋃ i, s_i / t.

Русский

Деление распределяется по объединению: деление объединения множеств на t равно объединению делений каждого множества на t.

LaTeX

$$$$ (\bigcup_i s_i) / t = \bigcup_i (s_i / t) $$$$

Lean4

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

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