Theorems · Theorem · order theory

exists_pow_lt_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 → y < 1 → ∃ n, y ^ n < x

For any y < 1 and any positive x, there exists n : ℕ with y ^ n < x.

Defined in

Mathlib.Algebra.Order.Archimedean.Basic

Cited by

16 results in Mathlib

Foundations

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

Assumes

SemifieldLinearOrderIsStrictOrderedRingArchimedeanExistsAddOfLE