Ioo_mem_nhdsLE_of_mem

Mathlib.Topology.Order.OrderClosed

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

English

If b ∈ Ioo a c, then Ioo a c is a left-neighborhood of b with respect to ≤-neighborhoods.

Русский

Если b ∈ Ioo a c, то Ioo a c является левой окрестностью b в отношении 𝓝[≤].

LaTeX

$$$(b \in Ioo(a,c)) \Rightarrow Ioo(a,c) \in \mathcal{N}_{[\le]}(b)$$$

Lean4

theorem Ioo_mem_nhdsLE_of_mem (H : b ∈ Ioo a c) : Ioo a c ∈ 𝓝[≤] b :=
  mem_of_superset (Ioc_mem_nhdsLE H.1) <| Ioc_subset_Ioo_right H.2

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

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

Разделы

Аффилиация

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