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 _)