natCast_mem_slitPlane — Mathlib

English

For any natural number n, the image ↑n lies in slitPlane if and only if n ≠ 0.

Русский

Для любого натурального числа n образ ↑n лежит в слитной плоскости тогда и только тогда, когда n ≠ 0.

LaTeX

$$$\\uparrow n \\in \\text{slitPlane} \\iff n \\neq 0$$$

Lean4

@[simp]
theorem natCast_mem_slitPlane {n : ℕ} : ↑n ∈ slitPlane ↔ n ≠ 0 := by
  simpa [pos_iff_ne_zero] using @ofReal_mem_slitPlane n

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