top_ne_coe

Mathlib.Data.ENat.Basic

URI: https://scilib.ai/kg/mathlib#ENat.top_ne_coe

English

For all a ∈ ℕ, top ≠ (a : ℕ∞).

Русский

Для любого a ∈ ℕ: ⊤ ≠ (a : ℕ∞).

LaTeX

$$$\\\\forall a \\\\in \\\\mathbb{N}, \\\\top \\\\neq (a \\\\in \\\\mathbb{N}_{\\\\infty}).$$$

Lean4

@[simp]
theorem top_ne_coe (a : ℕ) : ⊤ ≠ (a : ℕ∞) :=
  nofun

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

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

Разделы

Аффилиация

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