Theorems · Theorem · sequences and series
mul_pow_le_nat_floor_pow
∀ {c : ℝ}, 1 < c → ∀ (i : ℕ), (1 - c⁻¹) * c ^ i ≤ ↑⌊c ^ i⌋₊- Defined in
- Mathlib.Analysis.SpecificLimits.FloorPow
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 110 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites14
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- mul_oneproof · cited by 3,885
- Nat.cast_oneproof · cited by 2,501
- LT.lt.leproof · cited by 2,189
- eq_or_neproof · cited by 1,117
- pow_zeroproof · cited by 1,094
- zero_lt_oneproof · cited by 598
- LT.lt.transproof · cited by 370
- Nat.floorstatement and proof · cited by 215
- sub_le_sub_leftproof · cited by 43
- one_le_divproof · cited by 19
- le_self_pow₀proof · cited by 7
Cited by1
Results whose statement or proof uses this declaration.
- sum_div_nat_floor_pow_sq_le_div_sqproof · cited by 1