ofNat_ne_bot

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithBot.ofNat_ne_bot

English

If n ≥ 2, then instOfNatAtLeastTwo.ofNat n ≠ ⊥ in WithBot α.

Русский

Если n ≥ 2, то instOfNatAtLeastTwo.ofNat n ≠ ⊥ в WithBot α.

LaTeX

$$$$ \\forall n \\in \\mathbb{N},\\ [n.AtLeastTwo] \\mathrm{instOfNatAtLeastTwo}.ofNat(n) \\neq \\bot. $$$$

Lean4

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

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

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

Разделы

Аффилиация

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