English
Let p i be a predicate on ι, and s i subsets of X. Then the property P holds eventually on the union of those s i for which p i holds, if and only if for every i with p i, P holds eventually on s i.
Русский
Пусть p i — предикат на ι, и s i — множества в X. Тогда P выполняется практически на объединении s i, над которыми выполняется p i, тогда и только тогда, когда для каждого i с p i выполняется P на s i.
LaTeX
$$$(\\forall^\\infty x \\in 𝓝ˢ(⋃ i\\, (p i) \\,! s i),\\u00a0P x) \\leftrightarrow \\forall i, p i \\to (\\forall^\\infty x \\in 𝓝ˢ(s i),\\u00a0P x)$$$
Lean4
theorem eventually_nhdsSet_iUnion₂ {ι : Sort*} {p : ι → Prop} {s : ι → Set X} {P : X → Prop} :
(∀ᶠ x in 𝓝ˢ (⋃ (i) (_ : p i), s i), P x) ↔ ∀ i, p i → ∀ᶠ x in 𝓝ˢ (s i), P x := by
simp only [nhdsSet_iUnion, eventually_iSup]
