top_ne_ofNat

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

URI: https://scilib.ai/kg/mathlib#WithTop.top_ne_ofNat

English

Top is not equal to a natCast of a natural.

Русский

Верхний элемент не равен natCast натурального числа.

LaTeX

$$$\\\\forall n : \\\\mathbb{N} [n.AtLeastTwo], \\\\top \\\\neq (instOfNatAtLeastTwo.ofNat n)$$$

Lean4

@[simp]
theorem top_ne_ofNat (n : ℕ) [n.AtLeastTwo] : (⊤ : WithTop α) ≠ ofNat(n) :=
  top_ne_natCast n

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

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

Разделы

Аффилиация

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