English
If Nonempty ι and for all i, κ i nonempty, and every f i j is IsRelLowerSet with respect to P, then the double intersection over i and j of f i j is IsRelLowerSet with respect to P.
Русский
Пусть ι непусто, и для каждого i множества κ i непусты, тогда двукратное пересечение ⋂ i ⋂ j f i j является IsRelLowerSet относительно P.
LaTeX
$$$[Nonempty \ ι] [\forall i, Nonempty (κ i)] {f : \iota → κ i → Set α} (\forall i j, IsRelLowerSet (f i j) P) : IsRelLowerSet (\bigcap_{i} \bigcap_{j} f i j) P$$$
Lean4
protected theorem iInter₂ [Nonempty ι] [∀ i, Nonempty (κ i)] {f : ∀ i, κ i → Set α}
(hf : ∀ i j, IsRelLowerSet (f i j) P) : IsRelLowerSet (⋂ (i) (j), f i j) P :=
.iInter fun i ↦ .iInter (hf i)
