natCast_lt_top

Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

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

English

Any natural cast sits strictly below the top: (n : WithTop α) < ⊤.

Русский

Любое natCast строго ниже вершины: (n : WithTop α) < ⊤.

LaTeX

$$$\\\\forall n : \\\\mathbb{N}, (n : WithTop α) < \\top$$$

Lean4

@[simp]
theorem natCast_lt_top [LT α] (n : ℕ) : (n : WithTop α) < ⊤ :=
  coe_lt_top _

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

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

Разделы

Аффилиация

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