natCast_lt — Mathlib

English

For a succ-limit x, every natural number n satisfies n < x.

Русский

Для succ-limit x каждое натуральное число n удовлетворяет n < x.

LaTeX

$$$\\\\IsSuccLimit x \\\\land \\\\CanonicallyOrderedAdd α \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, n < x.$$$

Lean4

theorem natCast_lt [AddMonoidWithOne α] [SuccAddOrder α] [OrderBot α] [CanonicallyOrderedAdd α] (hx : IsSuccLimit x) :
    ∀ n : ℕ, n < x := by simpa [bot_eq_zero] using hx.add_natCast_lt hx.bot_lt

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