pi_Iic_mem_nhds — Mathlib

English

In a finite product of ordered spaces with OrderTopology, if all coordinate inequalities hold, then Icc of the coordinates lies in nhds x.

Русский

В конечном произведении упорядоченных пространств с OrderTopology, если все координаты удовлетворяют неравенствам, то Icc координат лежит в nhds x.

LaTeX

$$Icc a' b' ∈ 𝓝 x' when ∀ i, a'_i < x'_i and ∀ i, x'_i < b'_i$$

Lean4

theorem pi_Iic_mem_nhds (ha : ∀ i, x i < a i) : Iic a ∈ 𝓝 x :=
  pi_univ_Iic a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Iic_mem_nhds (ha _)

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