withTopEquiv_symm_ofNat — Mathlib

English

For any n with AtLeastTwo, the inverse maps ofNat(n) to OfNat.ofNat n: withTopEquiv.symm ofNat(n) = OfNat.ofNat n.

Русский

Для любого n при условии AtLeastTwo обратное отображение ofNat(n) даёт OfNat.ofNat n: withTopEquiv.symm ofNat(n) = OfNat.ofNat n.

LaTeX

$$$ \forall (n : \mathbb{N}) [n.\text{AtLeastTwo}],\; \mathrm{withTopEquiv}^{-1}(\operatorname{ofNat}(n)) = \operatorname{OfNat.ofNat}(n) $$$$

Lean4

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

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