grade_self

Mathlib.Order.Grade

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

English

In a graded order, grade a equals a when the grading is the identity; i.e., grade a = a for all a.

Русский

В градационном порядке при тождественной градации каждый элемент остается на месте: grade a = a.

LaTeX

$$$\\\\operatorname{grade}_{α}(a) = a$$$

Lean4

@[simp]
theorem grade_self (a : α) : grade α a = a :=
  rfl

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

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

Разделы

Аффилиация

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