English
Let f be a two-parameter family f(i, j) of sets indexed by i and κ i. If every f(i, j) is a RelLowerSet with respect to P, then the double union over i and j is a RelLowerSet with respect to P.
Русский
Пусть дано двумерное семейство множеств f(i, j). Если для всех i, j множества f(i, j) являются RelLowerSet относительно P, то двойное объединение ⋃_{i}⋃_{j} f(i, j) является RelLowerSet относительно P.
LaTeX
$$$\Bigl(\forall i, \forall j, IsRelLowerSet (f(i, j), P)\Bigr) \Rightarrow IsRelLowerSet\Bigl(\bigcup_{i} \bigcup_{j} f(i, j)\Bigr) P$$$
Lean4
protected theorem iUnion₂ {f : ∀ i, κ i → Set α} (hf : ∀ i j, IsRelLowerSet (f i j) P) :
IsRelLowerSet (⋃ (i) (j), f i j) P :=
.iUnion fun i ↦ .iUnion (hf i)
