grade_strictMono

Mathlib.Order.Grade

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

English

The grade map is strictly monotone: a < b implies grade(a) < grade(b).

Русский

Функция града монотонно строго возрастает: a < b тогда и только тогда grade(a) < grade(b).

LaTeX

$$$\text{StrictMono}(\mathrm{grade}):\; a < b \Rightarrow \mathrm{grade}(a) < \mathrm{grade}(b).$$$

Lean4

theorem grade_strictMono : StrictMono (grade 𝕆 : α → 𝕆) :=
  GradeOrder.grade_strictMono

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

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

Разделы

Аффилиация

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