pi_Ioi_mem_nhds — Mathlib

English

If each coordinate a_i is strictly less than x_i, then the product of the open upper intervals Ioi(a) is a neighborhood of x in the product topology.

Русский

Если для всех координат выполняется a_i < x_i, то произведение открытых верхних интервалов Ioi(a) является окрестностью x в произведении топологий.

LaTeX

$$$\left(\forall i, a_i < x_i\right) \rightarrow Ioi(a) \in \mathcal{N}(x)$$$

Lean4

theorem pi_Ioi_mem_nhds (ha : ∀ i, a i < x i) : Ioi a ∈ 𝓝 x :=
  pi_Iio_mem_nhds (X := fun i => (X i)ᵒᵈ) ha

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