pi_Iio_mem_nhds — Mathlib

English

If every coordinate x_i is strictly less than a_i, then the product of the open lower intervals Iio(a) is a neighborhood of x in the product topology.

Русский

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

LaTeX

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

Lean4

theorem pi_Iio_mem_nhds (ha : ∀ i, x i < a i) : Iio a ∈ 𝓝 x :=
  mem_of_superset (set_pi_mem_nhds finite_univ fun i _ ↦ Iio_mem_nhds (ha i)) (pi_univ_Iio_subset a)

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