coe_strictMono

Mathlib.Data.EReal.Basic

URI: https://scilib.ai/kg/mathlib#EReal.coe_strictMono

English

The embedding Real → EReal is strictly monotone.

Русский

Вложение Real → EReal строго монотонно.

LaTeX

$$$ \text{StrictMono}(\mathbb{R} \to \mathrm{EReal}). $$$

Lean4

theorem coe_strictMono : StrictMono Real.toEReal :=
  WithBot.coe_strictMono.comp WithTop.coe_strictMono

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

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

Разделы

Аффилиация

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