of — Mathlib · SciLib

English

The exact relation for the difference between v and its nth convergent is given by an explicit fraction depending on the nth fractional part and adjacent constants.

Русский

Разность между числом v и его n-ой сходной выражается через явную дробь, зависящую от дробной части и соседних констант.

LaTeX

$$$\\\\forall {K} {v} {n} [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K] {ifp : GenContFract.IntFractPair K},\n IntFractPair.stream v n = Some ifp \\\\Rightarrow \\\\text{равенство } v - (GenContFract.of v).convs n = \\\\ldots$$$

Lean4

/-- Creates the continued fraction of a value. -/
def of : ContFract K :=
  ⟨SimpContFract.of v, SimpContFract.of_isContFract v⟩

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