vsub_iUnion₂ — Mathlib

English

Let s, t i sets. Then s -ᵥ ⋃ i, ⋃ j t i j = ⋃ i, ⋃ j (s -ᵥ t i j).

Русский

Пусть s, t определяется по двойной индексации. Тогда s -ᵥ ⋃_{i,j} t(i,j) = ⋃_{i,j} (s -ᵥ t(i,j)).

LaTeX

$$$s -_v \\bigcup_{i} \\bigcup_{j} t(i,j) = \\bigcup_{i} \\bigcup_{j} (s -_v t(i,j))$$$

Lean4

theorem vsub_iUnion₂ (s : Set β) (t : ∀ i, κ i → Set β) : (s -ᵥ ⋃ i, ⋃ j, t i j) = ⋃ i, ⋃ j, s -ᵥ t i j :=
  image2_iUnion₂_right ..

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