grade_top — Mathlib

English

Let 𝕆 be an order on 𝕆 and α with a top element; the grade of the top element equals the top element: grade 𝕆 (⊤) = ⊤.

Русский

Пусть 𝕆 — порядок, у α есть верхняя граница; градационная карта отправляет ⊤ в ⊤: grade 𝕆(⊤) = ⊤.

LaTeX

$$$\\\\operatorname{grade}_{\\\\mathcal{O}}(\\\\top) = \\\\top$$$

Lean4

@[simp]
theorem grade_top [OrderTop 𝕆] [OrderTop α] [GradeMaxOrder 𝕆 α] : grade 𝕆 (⊤ : α) = ⊤ :=
  (isMax_top.grade _).eq_top

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