iUnion₂_congr — Mathlib

English

For two-parameter families s(i,j) and t(i,j), if ∀ i,j, s(i,j) = t(i,j), then ⋃_i ⋃_j s(i,j) = ⋃_i ⋃_j t(i,j).

Русский

Для двухпараметрических семей s(i,j) и t(i,j) если ∀ i,j, s(i,j) = t(i,j), то ⋃_i ⋃_j s(i,j) = ⋃_i ⋃_j t(i,j).

LaTeX

$$$$ \\forall i, \\forall j,\\ s(i,j) = t(i,j) \\Rightarrow \\bigcup_{i} \\bigcup_{j} s(i,j) = \\bigcup_{i} \\bigcup_{j} t(i,j) $$$$

Lean4

theorem iUnion₂_congr {s t : ∀ i, κ i → Set α} (h : ∀ i j, s i j = t i j) : ⋃ (i) (j), s i j = ⋃ (i) (j), t i j :=
  iUnion_congr fun i => iUnion_congr <| h i

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