natCast_lt_top

Mathlib.Data.Nat.PartENat

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

← MathLib Explorer

English

For every natural number x, (x : PartENat) < ⊤.

Русский

Для каждого x ∈ ℕ, (x : PartENat) < ⊤.

LaTeX

$$$ (x : \mathbb{N}) \;\Rightarrow\; (x : \mathrm{PartENat}) < \top $$$

Lean4

@[simp]
theorem natCast_lt_top (x : ℕ) : (x : PartENat) < ⊤ :=
  Ne.lt_top fun h => absurd (congr_arg Dom h) <| by simp only [dom_natCast]; exact true_ne_false

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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