dom_ofNat — Mathlib

English

If x ∈ ℕ has AtLeastTwo, then the element ofNat(x) in PartENat is defined.

Русский

Если x ∈ ℕ удовлетворяет условию AtLeastTwo, то элемент ofNat(x) в PartENat находится в области определения.

LaTeX

$$$\\\\forall x : \\\\mathbb{N}, [x.AtLeastTwo] \\\\Rightarrow (\\\\operatorname{ofNat}(x) : \\\\mathrm{PartENat}).\\\\Dom$$$

Lean4

@[simp]
theorem dom_ofNat (x : ℕ) [x.AtLeastTwo] : (ofNat(x) : PartENat).Dom :=
  trivial

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