isMin_grade_iff

Mathlib.Order.Grade

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

English

IsMin(grade(a)) iff IsMin(a); the grading preserves minimality.

Русский

IsMin(grade(a)) эквивалентно IsMin(a); градация сохраняет минимальность.

LaTeX

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

Lean4

@[simp]
theorem isMin_grade_iff : IsMin (grade 𝕆 a) ↔ IsMin a :=
  ⟨grade_strictMono.isMin_of_apply, IsMin.grade _⟩

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

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

Разделы

Аффилиация

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