Theorems · Definition · real analysis
Real.ofDigits
{b : ℕ} → (ℕ → Fin b) → ℝofDigits d is the real number 0.d₀d₁d₂... in base b.
We allow repeating representations like 0.999... here.
- Defined in
- Mathlib.Analysis.Real.OfDigits
- Cited by
- 14 results in Mathlib
- Foundations
- Depth 114 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement · cited by 25,697
- SummationFilter.unconditionalproof · cited by 2,068
- tsumproof · cited by 1,148
- Real.ofDigitsTermproof · cited by 15
Cited by16
Results whose statement or proof uses this declaration.
- Real.ofDigits_eq_sum_add_ofDigitsstatement · cited by 3
- Real.ofDigits_le_onestatement and proof · cited by 3
- Real.ofDigits_nonnegstatement · cited by 3
- Real.fromBinaryproof · cited by 2
- ofDigits_zero_two_sequence_mem_cantorSetstatement and proof · cited by 2
- Real.continuous_ofDigitsstatement and proof · cited by 1
- Real.ofDigits_SurjOnstatement · cited by 1
- Real.ofDigits_const_last_eq_onestatement · cited by 1
- Real.ofDigits_const_last_eq_one'statement and proof · cited by 1
- Real.ofDigits_digitsstatement · cited by 1
- ofDigits_cantorToTernarystatement · cited by 1
- Real.abs_ofDigits_sub_ofDigits_lestatement and proof · cited by 0