pi_Ico_mem_nhds — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem pi_Ico_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Ico a b ∈ 𝓝 x :=
  by
  refine mem_of_superset (set_pi_mem_nhds Set.finite_univ fun i _ => ?_) (pi_univ_Ico_subset a b)
  exact Ico_mem_nhds (ha i) (hb i)

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