of_isContFract — Mathlib

English

The simple continued fraction produced by v is a cont fract, i.e., its IsContFract property holds.

Русский

Простое продолженное дробление, порождаемое v, является непрерывной дробью.

LaTeX

$$$\\\\forall {K} (v : K) [Field K] [LinearOrder K] [IsStrictOrderedRing K] [FloorRing K], (SimpContFract.of v).IsContFract$$$

Lean4

theorem of_isContFract : (SimpContFract.of v).IsContFract := fun _ _ nth_partDen_eq =>
  lt_of_lt_of_le zero_lt_one (of_one_le_get?_partDen nth_partDen_eq)

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