nth_stream_fr_nonneg — Mathlib

English

The fractional parts of the stream are in the interval [0,1).

Русский

Дробные части потока находятся в интервале [0,1).

LaTeX

$$$0 \\leq f_r \\; \\text{and} \\; f_r < 1.$$$

Lean4

/-- Shows that the fractional parts of the stream are nonnegative. -/
theorem nth_stream_fr_nonneg {ifp_n : IntFractPair K} (nth_stream_eq : IntFractPair.stream v n = some ifp_n) :
    0 ≤ ifp_n.fr :=
  (nth_stream_fr_nonneg_lt_one nth_stream_eq).left

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