trNum_natEnd — Mathlib

English

Let n be a natural number and x be an element produced by the n-th construction trNum; then natEnd(x) is always false.

Русский

Пусть n — натуральное число и x — элемент, рождающийся во время конструирования trNum n; тогда natEnd(x) всегда ложь.

LaTeX

$$$\\forall n \\in \\mathbb{N}, \\forall x \\in \\operatorname{trNum}(n), \\operatorname{natEnd}(x) = \\text{false}$$$

Lean4

theorem trNum_natEnd : ∀ (n), ∀ x ∈ trNum n, natEnd x = false
  | Num.pos n, x, h => trPosNum_natEnd n x h

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