bot_ne_ofNat — Mathlib

English

In any AddMonoidWithOne α, for every natural number n with n ≥ 2, the bottom element ⊥ of WithBot α is different from the nat-casting of n, i.e., ⊥ ≠ ofNat(n) in WithBot α.

Русский

В любом моноиде с единицей α для любого натурального числа n ≥ 2 нижний элемент ⊥ в WithBot α не равен образованию n: ⊥ ≠ ofNat(n) в WithBot α.

LaTeX

$$$\\forall \\alpha\\, [AddMonoidWithOne \\alpha],\\ \\forall n \\in \\mathbb{N},\\ n \\ge 2\\;\\Rightarrow\\; (\\bot : \\mathrm{WithBot}\\ \\alpha) \\neq \\mathrm{ofNat}(n)$$$

Lean4

@[simp]
theorem bot_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊥ : WithBot α) ≠ ofNat(n) :=
  bot_ne_natCast n

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