lim_of_notMem_U — Mathlib

English

Let X be a topological space and c an UrysohnsCU object. Then for every point x in X that is not in c.U, the limit value c.lim x equals 1.

Русский

Пусть X — топологическое пространство и c — элемент Urysohns.CU. Тогда для каждого x ∈ X, не принадлежащего c.U, предел c.lim x равен 1.

LaTeX

$$$ x \notin c.U \Rightarrow c.lim x = 1 $$$

Lean4

theorem lim_of_notMem_U (c : CU P) (x : X) (h : x ∉ c.U) : c.lim x = 1 := by
  simp only [CU.lim, approx_of_notMem_U c _ h, ciSup_const]

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