Theorems · Theorem · order theory

exists_mem_Ico_zpow

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

Every positive x is between two successive integer powers of another y greater than one. This is the same as exists_mem_Ioc_zpow, but with ≤ and < the other way around.

Defined in

Mathlib.Algebra.Order.Archimedean.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingArchimedeanExistsAddOfLE