eventually_nhdsSet_iUnion — Mathlib

English

For a family s i of sets, the eventual property on the union equals the conjunction of eventual properties on each s i: ∀ᶠ x in 𝓝ˢ(⋃ i, s i), P x ↔ ∀ i, ∀ᶠ x in 𝓝ˢ(s i), P x.

Русский

Для семейства множеств s_i свойство P выполняется практически на объединении тогда и только тогда, когда выполняется практически для каждого i на s_i.

LaTeX

$$$(\\forall^\\infty x \\in 𝓝ˢ (\\bigcup_i s_i), P x) \\leftrightarrow \\forall i, \\forall^\\infty x \\in 𝓝ˢ (s_i), P x$$$

Lean4

theorem eventually_nhdsSet_iUnion {ι : Sort*} {s : ι → Set X} {P : X → Prop} :
    (∀ᶠ x in 𝓝ˢ (⋃ i, s i), P x) ↔ ∀ i, ∀ᶠ x in 𝓝ˢ (s i), P x := by simp only [nhdsSet_iUnion, eventually_iSup]

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