grade_lt_grade_iff

Mathlib.Order.Grade

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

English

grade a = grade b iff a = b.

Русский

grade(a) = grade(b) эквивалентно a = b.

LaTeX

$$$\mathrm{grade}(a) = \mathrm{grade}(b) \iff a = b.$$$

Lean4

@[simp]
theorem grade_lt_grade_iff : grade 𝕆 a < grade 𝕆 b ↔ a < b :=
  grade_strictMono.lt_iff_lt

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

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

Разделы

Аффилиация

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