coe_mono

Mathlib.Order.WithBot

URI: https://scilib.ai/kg/mathlib#WithTop.coe_mono

English

Monotonicity of the embedding a ↦ (a : WithTop α).

Русский

Монотонность отображения a ↦ (a : WithTop α).

LaTeX

$$$$ \\text{Monotone}(\\lambda a: \\alpha, a) \\Rightarrow \\text{Monotone}((a \\mapsto (a : WithTop \\alpha))). $$$$

Lean4

theorem coe_mono : Monotone (fun a : α => (a : WithTop α)) := fun _ _ => coe_le_coe.2

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

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

Разделы

Аффилиация

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