isMax_grade_iff

Mathlib.Order.Grade

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

English

IsMax(grade(a)) iff IsMax(a).

Русский

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

LaTeX

$$$\text{IsMax}(\mathrm{grade}(a)) \iff \text{IsMax}(a).$$$

Lean4

@[simp]
theorem isMax_grade_iff : IsMax (grade 𝕆 a) ↔ IsMax a :=
  ⟨grade_strictMono.isMax_of_apply, IsMax.grade _⟩

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

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

Разделы

Аффилиация

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