approx_mono

Mathlib.Topology.UrysohnsLemma

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

English

For a fixed x, the map n ↦ approx n x is monotone nondecreasing.

Русский

Для фиксированного x отображение n ↦ approx n x неубывает.

LaTeX

$$$Monotone\\ (n \\mapsto approx(n,c,x))$$$

Lean4

theorem approx_mono (c : CU P) (x : X) : Monotone fun n => c.approx n x :=
  monotone_nat_of_le_succ fun n => c.approx_le_succ n x

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

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

Разделы

Аффилиация

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