English
Let s and t be subsets of a topological space X and p a predicate on X. The property p holds eventually on the union s ∪ t with respect to 𝓝ˢ(s ∪ t) if and only if p holds eventually on s and on t separately with respect to 𝓝ˢ s and 𝓝ˢ t.
Русский
Пусть s и t — подмножества X; для предиката p верно: p выполняется практически на объединении s ∪ t тогда и только тогда, когда p выполняется практически на s и на t по отдельности.
LaTeX
$$$(\\forall^\\infty x \\in 𝓝ˢ (s \\cup t),\\ p(x)) \\leftrightarrow (\\forall^\\infty x \\in 𝓝ˢ s,\u00a0p(x)) \\land (\\forall^\\infty x \\in 𝓝ˢ t,\u00a0p(x))$$$
Lean4
theorem union_nhdsSet {p : X → Prop} : (∀ᶠ x in 𝓝ˢ (s ∪ t), p x) ↔ (∀ᶠ x in 𝓝ˢ s, p x) ∧ ∀ᶠ x in 𝓝ˢ t, p x := by
rw [nhdsSet_union, eventually_sup]
