grade

Mathlib.Order.Grade

URI: https://scilib.ai/kg/mathlib#IsMax.grade

English

If a is maximal (IsMax) then grade(a) is maximal in the graded order.

Русский

Если a максимален, то grade(a) максимален в градуированном порядке.

LaTeX

$$$\text{IsMax}(a) \Rightarrow \text{IsMax}(\mathrm{grade}(a)).$$$

Lean4

protected theorem grade (h : IsMax a) : IsMax (grade 𝕆 a) :=
  GradeMaxOrder.isMax_grade h

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

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

Разделы

Аффилиация

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