grade_bot — Mathlib

English

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

Русский

Пусть 𝕆 — частичный/полный порядок, α имеет нижнюю границу; градационная карта применима к ⊥ и возвращает ⊥: grade 𝕆(⊥) = ⊥.

LaTeX

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

Lean4

@[simp]
theorem grade_bot [OrderBot 𝕆] [OrderBot α] [GradeMinOrder 𝕆 α] : grade 𝕆 (⊥ : α) = ⊥ :=
  (isMin_bot.grade _).eq_bot

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