grade

Mathlib.Order.Grade

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

English

If a is minimal (IsMin) then grade(a) is minimal in the graded order.

Русский

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

LaTeX

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

Lean4

protected theorem grade (h : IsMin a) : IsMin (grade 𝕆 a) :=
  GradeMinOrder.isMin_grade h

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

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

Разделы

Аффилиация

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