union — Mathlib

English

If p holds eventually with respect to 𝓝ˢ s and with respect to 𝓝ˢ t, then p holds eventually with respect to 𝓝ˢ (s ∪ t).

Русский

Если для множества s и t предикат p выполняется практически на 𝓝ˢ s и на 𝓝ˢ t, то p выполняется практически на 𝓝ˢ (s ∪ t).

LaTeX

$$$(\\forall^\\infty x \\in 𝓝ˢ s,\u00a0p(x)) \\to (\\forall^\\infty x \\in 𝓝ˢ t,\u00a0p(x)) \\to \\forall^\\infty x \\in 𝓝ˢ (s \\cup t),\\u00a0p(x)$$$

Lean4

theorem union {p : X → Prop} (hs : ∀ᶠ x in 𝓝ˢ s, p x) (ht : ∀ᶠ x in 𝓝ˢ t, p x) : ∀ᶠ x in 𝓝ˢ (s ∪ t), p x :=
  Filter.Eventually.union_nhdsSet.mpr ⟨hs, ht⟩

Похожие утверждения