grade_eq_grade_iff

Mathlib.Order.Grade

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

English

The grade function is injective: if grade 𝕆 a = grade 𝕆 b, then a = b.

Русский

Функция града инъективна: если grade 𝕆 a = grade 𝕆 b, то a = b.

LaTeX

$$$grade\, 𝕆\ a = grade\, 𝕆\ b \iff a = b$$$

Lean4

@[simp]
theorem grade_eq_grade_iff : grade 𝕆 a = grade 𝕆 b ↔ a = b :=
  grade_injective.eq_iff

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

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

Разделы

Аффилиация

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