lt_sub_natCast — Mathlib

English

If x is pred-prelimit and x < y, then for every n ∈ N, x < y − n.cast.

Русский

Если x — pred-prelimit и x < y, то для каждого n ∈ N имеет x < y − n.cast.

LaTeX

$$$\\\\IsPredPrelimit x \\\\land x < y \\\\Rightarrow \\\\forall n \\\\in \\\\mathbb{N}, x < y - n.$$$

Lean4

theorem lt_sub_natCast [AddCommGroupWithOne α] [PredSubOrder α] (hx : IsPredPrelimit x) (hy : x < y) :
    ∀ n : ℕ, x < y - n
  | 0 => by simpa
  | n + 1 => by
    rw [Nat.cast_add_one, ← sub_sub]
    exact hx.lt_sub_one (hx.lt_sub_natCast hy n)

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