Theorems · Theorem · number theory

GenContFract.IntFractPair.nth_stream_fr_nonneg_lt_one

∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K] {ifp_n : GenContFract.IntFractPair K},
  GenContFract.IntFractPair.stream v n = some ifp_n → 0 ≤ ifp_n.fr ∧ ifp_n.fr < 1

Shows that the fractional parts of the stream are in [0,1).

Defined in: Mathlib.Algebra.ContinuedFractions.Computation.Approximations
Cited by: 4 results in Mathlib
Foundations: Depth 48 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Field LinearOrder IsStrictOrderedRing FloorRing

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites11

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

LinearOrderstatement and proof · cited by 8,572
Fieldstatement and proof · cited by 7,404
IsStrictOrderedRingstatement and proof · cited by 2,490
FloorRingstatement and proof · cited by 405
GenContFract.IntFractPairstatement and proof · cited by 45
GenContFract.IntFractPair.streamstatement and proof · cited by 37
GenContFract.IntFractPair.frstatement and proof · cited by 25
GenContFract.IntFractPair.ofproof · cited by 22
Int.fract_lt_oneproof · cited by 20
Int.fract_nonnegproof · cited by 17
GenContFract.IntFractPair.succ_nth_stream_eq_some_iffproof · cited by 8

Cited by4

Results whose statement or proof uses this declaration.

GenContFract.IntFractPair.nth_stream_fr_nonnegproof · cited by 3
GenContFract.IntFractPair.exists_nth_stream_eq_none_of_ratproof · cited by 1
GenContFract.IntFractPair.stream_succ_nth_fr_num_lt_nth_fr_num_ratproof · cited by 1
GenContFract.IntFractPair.nth_stream_fr_lt_oneproof · cited by 1