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