grade_le_grade_iff

Mathlib.Order.Grade

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

English

grade a ≤ grade b iff a ≤ b in the base order.

Русский

grade(a) ≤ grade(b) эквивалентно a ≤ b в базовом порядке.

LaTeX

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

Lean4

@[simp]
theorem grade_le_grade_iff : grade 𝕆 a ≤ grade 𝕆 b ↔ a ≤ b :=
  grade_strictMono.le_iff_le

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

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

Разделы

Аффилиация

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