ofSeq_surjective — Mathlib

English

The map ofSeq is surjective: every hyperreal number is represented by some real sequence.

Русский

Карта ofSeq сюръективна: каждый гиперреал представлен последовательностью вещественных чисел.

LaTeX

$$$\mathrm{ofSeq}$ surjective: \forall h \\in \mathbb{R}^{*}, \\exists f:\mathbb{N} \to \mathbb{R}, \mathrm{ofSeq}(f) = h$$$

Lean4

theorem ofSeq_surjective : Function.Surjective ofSeq :=
  Quot.exists_rep

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