approx_le_lim

Mathlib.Topology.UrysohnsLemma

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

English

For any natural number n, the nth approximation c.approx n x is bounded above by the limit: c.approx n x ≤ c.lim x.

Русский

Для любого натурального числа n приближение c.approx n x не превышает предела: c.approx n x ≤ c.lim x.

LaTeX

$$$ c.approx n x \le c.lim x $$$

Lean4

theorem approx_le_lim (c : CU P) (x : X) (n : ℕ) : c.approx n x ≤ c.lim x :=
  le_ciSup (c.bddAbove_range_approx x) _

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

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

Разделы

Аффилиация

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