pi_Ioo_mem_nhds — Mathlib

English

If a_i < x_i < b_i for all i, then the product Ioo(a,b) is a neighborhood of x.

Русский

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

LaTeX

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

Lean4

theorem pi_Ioo_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ioo a b ∈ 𝓝 x :=
  by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ioo_subset a b)
  exact Ioo_mem_nhds (ha i) (hb i)

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