Theorems · Theorem · order theory

exists_nat_pow_near_of_lt_one

∀ {K : Type u_4} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K}
  [ExistsAddOfLE K], 0 < x → x ≤ 1 → 0 < y → y < 1 → ∃ n, y ^ (n + 1) < x ∧ x ≤ y ^ n

Given x and y between 0 and 1, x is between two successive powers of y. This is the same as exists_nat_pow_near, but for elements between 0 and 1

Defined in

Mathlib.Algebra.Order.Archimedean.Basic

Cited by

2 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemifieldLinearOrderIsStrictOrderedRingArchimedeanExistsAddOfLE