toWithTop_ofNat

Mathlib.Data.Nat.PartENat

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

← MathLib Explorer

English

If n ≥ 2, then toWithTop(ofNat(n)) = OfNat.ofNat(n).

Русский

Если n ≥ 2, то toWithTop(ofNat(n)) = OfNat.ofNat(n).

LaTeX

$$$\\forall n \\in \\mathbb{N}, n \\ge 2 \\Rightarrow \\operatorname{toWithTop}(\\operatorname{ofNat}(n)) = \\operatorname{OfNat}(n)$$$

Lean4

@[simp]
theorem toWithTop_ofNat (n : ℕ) [n.AtLeastTwo] {_ : Decidable (OfNat.ofNat n : PartENat).Dom} :
    toWithTop (ofNat(n) : PartENat) = OfNat.ofNat n :=
  toWithTop_natCast' n

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

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

Разделы

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

Аффилиация

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