vsub_iUnion — Mathlib

English

The vsub over an iUnion equals the iUnion over vsub with each set: vsub_iUnion(s, t) = iUnion (vsub s (t i)).

Русский

Область вычитания вектором над объединением равна объединению по i от векторного вычитания: vsub_iUnion(s,t) = ∪_i (s -ᵥ t_i).

LaTeX

$$$\\operatorname{vsub}\\_{\!}(\\operatorname{iUnion}(s_i), t) = \\operatorname{iUnion}(\\lambda i, \\operatorname{vsub}(s_i, t))$$$

Lean4

theorem vsub_iUnion (s : Set β) (t : ι → Set β) : (s -ᵥ ⋃ i, t i) = ⋃ i, s -ᵥ t i :=
  image2_iUnion_right ..

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