isClosed_iUnion₂ — Mathlib

English

The union over i and j of closed sets f(i,j) is closed if all f(i,j) are closed.

Русский

Объединение по двум индексам замкнуто, если каждая пара f(i,j) замкнута.

LaTeX

$$$\Big(\forall i,\forall j, IsClosed(f(i,j))\Big) \Rightarrow IsClosed(\bigcup_i\bigcup_j f(i,j))$$$

Lean4

theorem isClosed_iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsClosed (f i j)) : IsClosed (⋃ i, ⋃ j, f i j) :=
  isClosed_iUnion fun _ ↦ isClosed_iUnion <| hf _

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