grade_mono

Mathlib.Order.Grade

URI: https://scilib.ai/kg/mathlib#grade_mono

English

The grade map is monotone with respect to the base order: a ≤ b implies grade(a) ≤ grade(b).

Русский

Функция града монотонна по базовому порядку: a ≤ b ⇒ grade(a) ≤ grade(b).

LaTeX

$$$a \le b \Rightarrow \mathrm{grade}(a) \le \mathrm{grade}(b).$$$

Lean4

theorem grade_mono [PartialOrder α] [GradeOrder 𝕆 α] : Monotone (grade 𝕆 : α → 𝕆) :=
  grade_strictMono.monotone

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

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

Разделы

Аффилиация

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