instNeBotNhdsWithinIoi — Mathlib

English

If for all i, nhdsWithin (x_i) (Ioi (x_i)) is nontrivial, then nhdsWithin x (Set.Ioi x) is nontrivial: (nhdsWithin x (Set.Ioi x)).NeBot.

Русский

Если во всех координатах существуют непустые окрестности в Ioi(x_i), то в произведении непустая окрестность в Ioi(x).

LaTeX

$$$$ (\\\\mathcal{N}_{>}(x)) \\\\text{ NeBot } \\\\Rightarrow (\\\\mathcal{N}_{> } x).NeBot.$$$$

Lean4

instance instNeBotNhdsWithinIoi [Nonempty ι] [∀ i, Preorder (X i)] {x : ∀ i, X i} [∀ i, (𝓝[>] x i).NeBot] :
    (𝓝[>] x).NeBot :=
  Pi.instNeBotNhdsWithinIio (X := fun i ↦ (X i)ᵒᵈ) (x := fun i ↦ OrderDual.toDual (x i))

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