pi_Ioc_mem_nhds — Mathlib

English

If each coordinate satisfies a_i < x_i < b_i, then the product of the open-closed interval Ioc(a,b) is a neighborhood of x.

Русский

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

LaTeX

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

Lean4

theorem pi_Ioc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioc a b ∈ 𝓝 x :=
  by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioc_subset a b)
  exact Ioc_mem_nhds (ha i) (hb i)

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