nth_stream_fr_lt_one — Mathlib

English

Let the nth term of the IntFractPair stream be defined as some ifp_n. Then the fractional part fr of ifp_n lies strictly between 0 and 1, i.e., 0 ≤ fr < 1; in particular fr < 1.

Русский

Пусть n-й элемент последовательности IntFractPair задан как some ifp_n. Тогда дробная часть fr этого элемента удовлетворяет 0 ≤ fr < 1; в частности fr < 1.

LaTeX

$$$\\\\forall K v n \\\\[Field K] \\\\[LinearOrder K] \\\\[IsStrictOrderedRing K] \\\\[FloorRing K], \\\\forall ifp_n : GenContFract.IntFractPair K, IntFractPair.stream \\\\mathbf{v} n = Some \\\\mathbf{ifp_n} \\\\Rightarrow ///// ifp_n.fr < 1$$$

Lean4

/-- Shows that the fractional parts of the stream are smaller than one. -/
theorem nth_stream_fr_lt_one {ifp_n : IntFractPair K} (nth_stream_eq : IntFractPair.stream v n = some ifp_n) :
    ifp_n.fr < 1 :=
  (nth_stream_fr_nonneg_lt_one nth_stream_eq).right

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