English
If for all i' and j' there exists i and j with s(i)(j) ⊆ t(i')(j'), then ⋂_i ⋂_j s(i)(j) ⊆ ⋂_{i'} ⋂_{j'} t(i')(j').
Русский
Если для всех i', j' существует i, j с s(i)(j) ⊆ t(i')(j'), то ⋂_i ⋂_j s(i)(j) ⊆ ⋂_{i'} ⋂_{j'} t(i')(j').
LaTeX
$$$\forall i'\!\ j',\ exists\ i,\ j,\ s_{ij} \subseteq t_{i' j'} \Rightarrow \bigcap_i\bigcap_j s_{ij} \subseteq \bigcap_{i'}\bigcap_{j'} t_{i' j'}$$$
Lean4
theorem iInter₂_mono' {s : ∀ i, κ i → Set α} {t : ∀ i', κ' i' → Set α} (h : ∀ i' j', ∃ i j, s i j ⊆ t i' j') :
⋂ (i) (j), s i j ⊆ ⋂ (i') (j'), t i' j' :=
subset_iInter₂_iff.2 fun i' j' =>
let ⟨_, _, hst⟩ := h i' j'
(iInter₂_subset _ _).trans hst
