addNSMul — Mathlib

English

In an Archimedean ordered group, with δ > 0, there exists m such that for all n ≥ m, addNSMul h δ n = b.

Русский

В упорядоченной архимедовой группе, при δ > 0, существует m такой, что для всех n ≥ m выполняется addNSMul h δ n = b.

LaTeX

$$∃ m, ∀ n ≥ m, addNSMul h δ n = b$$

Lean4

/-- When `h : a ≤ b` and `δ > 0`, `addNSMul h δ` is a sequence of points in the closed interval
`[a,b]`, which is initially equally spaced but eventually stays at the right endpoint `b`. -/
def addNSMul (δ : α) (n : ℕ) : Icc a b :=
  projIcc a b h (a + n • δ)

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