lim_mem_Icc

Mathlib.Topology.UrysohnsLemma

URI: https://scilib.ai/kg/mathlib#Urysohns.CU.lim_mem_Icc

English

For any c and x, the limit c.lim x lies in the closed interval Icc(0,1); i.e., c.lim x ∈ [0,1].

Русский

Для любого c и x предел c.lim x принадлежит замкнутому промежутку [0,1].

LaTeX

$$$ c.lim x \in Icc (0 : \mathbb{R}) 1 $$$

Lean4

theorem lim_mem_Icc (c : CU P) (x : X) : c.lim x ∈ Icc (0 : ℝ) 1 :=
  ⟨c.lim_nonneg x, c.lim_le_one x⟩

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

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

Разделы

Аффилиация

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