mk_pos — Mathlib

English

A real number represented by a Cauchy sequence is positive iff the sequence is eventually positive (Pos f).

Русский

Число действительное, полученное из последовательности Коши, положительно тогда и только тогда, когда последовательность в итоге положительна (Pos f).

LaTeX

$$$$0 < \\operatorname{mk}(f) \\iff \\mathrm{Pos}(f)$$$$

Lean4

@[simp]
theorem mk_pos {f : CauSeq ℚ abs} : 0 < mk f ↔ Pos f :=
  by
  rw [← mk_zero, mk_lt]
  exact iff_of_eq (congr_arg Pos (sub_zero f))

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