withTopEquiv_ofNat

Mathlib.Data.Nat.PartENat

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

English

For any n ∈ ℕ with AtLeastTwo, withTopEquiv(ofNat(n)) = OfNat.ofNat(n).

Русский

Для любого n ∈ ℕ c условием n ≥ 2, withTopEquiv(ofNat(n)) = OfNat.ofNat(n).

LaTeX

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

Lean4

theorem withTopEquiv_ofNat (n : Nat) [n.AtLeastTwo] : withTopEquiv ofNat(n) = OfNat.ofNat n := by simp

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

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

Разделы

Аффилиация

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