ofSeq_lt_ofSeq — Mathlib

English

The order of hyperreal numbers from sequences matches eventual pointwise order: ofSeq f < ofSeq g iff f(n) < g(n) eventually along the hyperfilter.

Русский

Порядок гиперреалов полученных из последовательностей соответствует почти везде по отношению к асимптотическому порядку: ofSeq f < ofSeq g тогда и только тогда, когда f(n) < g(n) для единообразно больших n.

LaTeX

$$$\mathrm{ofSeq}(f) < \mathrm{ofSeq}(g) \\iff \\forall^\\infty n \\in \\mathrm{hyperfilter}(\\mathbb{N}), \\ f(n) < g(n)$$$

Lean4

theorem ofSeq_lt_ofSeq {f g : ℕ → ℝ} : ofSeq f < ofSeq g ↔ ∀ᶠ n in hyperfilter ℕ, f n < g n :=
  Germ.coe_lt

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