English
If for all i, nhdsWithin (x_i) (Iio (x_i)) is nontrivial, then nhdsWithin x (range pi s) (or Iio x) is nontrivial in the product space: (nhdsWithin x (Set.univ.pi s)).NeBot.
Русский
Если во всех координатах существуют непустые окрестности в множестве Iio(x_i), то в произведении также существует непустая окрестность в Iio(x).
LaTeX
$$$$ (\\\\mathcal{N}_{<}(x)) \\\\text{ NeBot } \\\\Rightarrow (\\\\mathcal{N}_{<} x).NeBot.$$$$
Lean4
instance instNeBotNhdsWithinIio [Nonempty ι] [∀ i, Preorder (X i)] {x : ∀ i, X i} [∀ i, (𝓝[<] x i).NeBot] :
(𝓝[<] x).NeBot :=
have : (𝓝[pi univ fun i ↦ Iio (x i)] x).NeBot := inferInstance
this.mono <| nhdsWithin_mono _ fun _y hy ↦ lt_of_strongLT fun i ↦ hy i trivial
