lim_of_mem_C

Mathlib.Topology.UrysohnsLemma

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

English

If x ∈ C, then the limit c.lim x is 0.

Русский

Если x ∈ C, то предел c.lim x равен 0.

LaTeX

$$$c.lim x = 0 \\quad\\text{если } x \\in c.C$$$

Lean4

theorem lim_of_mem_C (c : CU P) (x : X) (h : x ∈ c.C) : c.lim x = 0 := by
  simp only [CU.lim, approx_of_mem_C, h, ciSup_const]

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

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

Разделы

Аффилиация

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