mathlib documentation

algebra.archimedean

@[class]
structure archimedean (α : Type u_2) [ordered_add_comm_monoid α] :
Prop
  • arch : ∀ (x : α) {y : α}, 0 < y(∃ (n : ), x n •ℕ y)

An ordered additive commutative monoid is called archimedean if for any two elements x, y such that 0 < y there exists a natural number n such that x ≤ n •ℕ y.

Instances
theorem decidable_linear_ordered_add_comm_group.exists_int_smul_near_of_pos {α : Type u_1} [decidable_linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (g : α) :
∃ (k : ), k •ℤ a g g < (k + 1) •ℤ a

An archimedean decidable linearly ordered add_comm_group has a version of the floor: for a > 0, any g in the group lies between some two consecutive multiples of a.

theorem decidable_linear_ordered_add_comm_group.exists_int_smul_near_of_pos' {α : Type u_1} [decidable_linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (g : α) :
∃ (k : ), 0 g - k •ℤ a g - k •ℤ a < a

theorem exists_nat_gt {α : Type u_1} [linear_ordered_semiring α] [archimedean α] (x : α) :
∃ (n : ), x < n

theorem exists_nat_ge {α : Type u_1} [linear_ordered_semiring α] [archimedean α] (x : α) :
∃ (n : ), x n

theorem add_one_pow_unbounded_of_pos {α : Type u_1} [linear_ordered_semiring α] [archimedean α] (x : α) {y : α} :
0 < y(∃ (n : ), x < (y + 1) ^ n)

theorem pow_unbounded_of_one_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) {y : α} :
1 < y(∃ (n : ), x < y ^ n)

theorem exists_nat_pow_near {α : Type u_1} [linear_ordered_ring α] [archimedean α] {x y : α} :
1 x1 < y(∃ (n : ), y ^ n x x < y ^ (n + 1))

Every x greater than or equal to 1 is between two successive natural-number powers of every y greater than one.

theorem exists_int_gt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (n : ), x < n

theorem exists_int_lt {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (n : ), n < x

theorem exists_floor {α : Type u_1} [linear_ordered_ring α] [archimedean α] (x : α) :
∃ (fl : ), ∀ (z : ), z fl z x

theorem exists_int_pow_near {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] {x y : α} :
0 < x1 < y(∃ (n : ), y ^ n x x < y ^ (n + 1))

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

theorem exists_int_pow_near' {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] {x y : α} :
0 < x1 < y(∃ (n : ), y ^ n < x x y ^ (n + 1))

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

theorem sub_floor_div_mul_nonneg {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) {y : α} :
0 < y0 x - (x / y) * y

theorem sub_floor_div_mul_lt {α : Type u_1} [linear_ordered_field α] [floor_ring α] (x : α) {y : α} :
0 < yx - (x / y) * y < y

@[instance]

@[instance]

A linear ordered archimedean ring is a floor ring. This is not an instance because in some cases we have a computable floor function.

Equations
theorem archimedean_iff_nat_lt {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (n : ), x < n

theorem archimedean_iff_nat_le {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (n : ), x n

theorem exists_rat_gt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :
∃ (q : ), x < q

theorem archimedean_iff_rat_lt {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (q : ), x < q

theorem archimedean_iff_rat_le {α : Type u_1} [linear_ordered_field α] :
archimedean α ∀ (x : α), ∃ (q : ), x q

theorem exists_rat_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :
∃ (q : ), q < x

theorem exists_rat_btwn {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} :
x < y(∃ (q : ), x < q q < y)

theorem exists_nat_one_div_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {ε : α} :
0 < ε(∃ (n : ), 1 / (n + 1) < ε)

theorem exists_pos_rat_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {x : α} :
0 < x(∃ (q : ), 0 < q q < x)

@[simp]
theorem rat.cast_floor {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : ) :

def round {α : Type u_1} [discrete_linear_ordered_field α] [floor_ring α] :
α →

round rounds a number to the nearest integer. round (1 / 2) = 1

Equations
theorem abs_sub_round {α : Type u_1} [discrete_linear_ordered_field α] [floor_ring α] (x : α) :
abs (x - (round x)) 1 / 2

theorem exists_rat_near {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (x : α) {ε : α} :
0 < ε(∃ (q : ), abs (x - q) < ε)

@[instance]

@[simp]
theorem rat.cast_round {α : Type u_1} [discrete_linear_ordered_field α] [archimedean α] (x : ) :