bddAbove_range_approx

Mathlib.Topology.UrysohnsLemma

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

English

The set {approx n x | n ∈ ℕ} is bounded above by 1 for each x.

Русский

Множество {аппроксимация n x} ограничено сверху единицей для каждого x.

LaTeX

$$$BddAbove(\\{ c.approx n x \\mid n \\in \\mathbb{N} \\})$$$

Lean4

theorem bddAbove_range_approx (c : CU P) (x : X) : BddAbove (range fun n => c.approx n x) :=
  ⟨1, fun _ ⟨n, hn⟩ => hn ▸ c.approx_le_one n x⟩

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

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

Разделы

Аффилиация

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