Icc_mem_nhdsGT_of_mem

Mathlib.Topology.Order.OrderClosed

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

English

If b ∈ Ico(a, c), then Icc(a, c) is a neighborhood of b on the right.

Русский

Если b ∈ Ico(a, c), то Icc(a, c) является окрестностью b справа.

LaTeX

$$$b \in Ico(a, c) \rightarrow Icc(a, c) \in 𝓝[>] b$$$

Lean4

theorem Icc_mem_nhdsGT_of_mem (H : b ∈ Ico a c) : Icc a c ∈ 𝓝[>] b :=
  mem_of_superset (Ioo_mem_nhdsGT_of_mem H) Ioo_subset_Icc_self

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

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

Разделы

Аффилиация

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