pi_Ici_mem_nhds

Mathlib.Topology.Order.Basic

URI: https://scilib.ai/kg/mathlib#pi_Ici_mem_nhds

English

For a product of ordered spaces with OrderTopology, if a_i < x_i holds for all i, then the closed-infinite interval Ici(a) lies in nhds x.

Русский

Если для всех i выполняется a_i < x_i, тогда Ici(a) ∈ nhds x.

LaTeX

$$Ici a ∈ 𝓝 x when ∀ i, a_i < x_i$$

Lean4

theorem pi_Ici_mem_nhds (ha : ∀ i, a i < x i) : Ici a ∈ 𝓝 x :=
  pi_univ_Ici a ▸ set_pi_mem_nhds (Set.toFinite _) fun _ _ => Ici_mem_nhds (ha _)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru