instNeBotNhdsWithinUnivPi — Mathlib

English

If each coordinate has a nontrivial nhdsWithin within s_i, then the product’s nhdsWithin on the unrestricted pi-space is nontrivial: if ∀ i, (nhdsWithin (x_i) (s_i)).NeBot, then (nhdsWithin x (pi univ s)).NeBot.

Русский

Если для каждой координаты i непустые окрестности внутри s_i, то в произведении фильтр окрестностей внутри pi univ s также непустой.

LaTeX

$$$$\\left( \\forall i, (\\\\mathcal{N}_{s_i}(x_i)).NeBot \\right) \\\\Rightarrow (\\\\mathcal{N}_{\\\\pi univ s}(x)).NeBot.$$$$

Lean4

instance instNeBotNhdsWithinUnivPi {s : ∀ i, Set (X i)} {x : ∀ i, X i} [∀ i, (𝓝[s i] x i).NeBot] :
    (𝓝[pi univ s] x).NeBot := by simpa [nhdsWithin_pi_neBot]

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