orderBot — Mathlib

English

There is a bottom element in DegLex(α →₀ ℕ), defined as toDegLex(0), and it is a bottom regarding the order.

Русский

В DegLex(α →₀ ℕ) существует нижний элемент, равный toDegLex(0), и он минимален по порядку.

LaTeX

$$$\mathrm{bot} := \mathrm{toDegLex}(0) \quad\land\quad \forall x,\ \mathrm{bot} \le x$$$

Lean4

noncomputable instance orderBot : OrderBot (DegLex (α →₀ ℕ))
    where
  bot := toDegLex (0 : α →₀ ℕ)
  bot_le
    x := by
    simp only [le_iff, ofDegLex_toDegLex, toLex_zero, degree_zero]
    rcases eq_zero_or_pos (ofDegLex x).degree with (h | h)
    · simp only [h, lt_self_iff_false, true_and, false_or]
      exact bot_le
    · simp [h]

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