ratLt'_bddAbove

Mathlib.Data.Real.Embedding

URI: https://scilib.ai/kg/mathlib#Archimedean.ratLt'_bddAbove

English

The primed version ratLt' x is bounded above by some real number.

Русский

Упрощённое множество ratLt'(x) ограничено сверху некоторым числом в ℝ.

LaTeX

$$$\exists b \in \mathbb{R}, \; BddAbove(\operatorname{ratLt'}(x))$$$

Lean4

theorem ratLt'_bddAbove (x : M) : BddAbove (ratLt' x) :=
  Monotone.map_bddAbove Rat.cast_mono <| ratLt_bddAbove x

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

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

Разделы

Аффилиация

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