Theorems · Theorem · order theory

uniform_continuous_npow_on_bounded

∀ {α : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (B : α) {ε : α},
  0 < ε → ∀ (n : ℕ), ∃ δ > 0, ∀ (q r : α), |r| ≤ B → |q - r| ≤ δ → |q ^ n - r ^ n| < ε

Defined in

Mathlib.Algebra.Order.Field.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderIsStrictOrderedRing