pi_Icc_mem_nhds — Mathlib

English

In a finite product of linear orders with OrderTopology, if a_i < x_i and x_i < b_i hold for all i, then Icc(a,b) is in nhds x.

Русский

В произведении линейных порядков, если a_i < x_i < b_i для всех i, то Icc(a,b) ∈ nhds x.

LaTeX

$$Icc a b ∈ 𝓝 x when ∀ i, a_i < x_i and ∀ i, x_i < b_i$$

Lean4

theorem pi_Icc_mem_nhds (ha : ∀ i, a i < x i) (hb : ∀ i, x i < b i) : Icc a b ∈ 𝓝 x :=
  pi_univ_Icc a b ▸ set_pi_mem_nhds finite_univ fun _ _ => Icc_mem_nhds (ha _) (hb _)

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