@[class]
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.
theorem
add_one_pow_unbounded_of_pos
{α : Type u_1}
[linear_ordered_semiring α]
[archimedean α]
(x : α)
{y : α}
(hy : 0 < y) :
theorem
pow_unbounded_of_one_lt
{α : Type u_1}
[linear_ordered_ring α]
[archimedean α]
(x : α)
{y : α}
(hy1 : 1 < y) :
theorem
exists_nat_pow_near
{α : Type u_1}
[linear_ordered_ring α]
[archimedean α]
{x y : α}
(hx : 1 ≤ x)
(hy : 1 < y) :
Every x greater than or equal to 1 is between two successive natural-number powers of every y greater than one.
theorem
exists_int_pow_near
{α : Type u_1}
[discrete_linear_ordered_field α]
[archimedean α]
{x y : α}
(hx : 0 < x)
(hy : 1 < y) :
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 : α}
(hx : 0 < x)
(hy : 1 < y) :
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 : α}
(hy : 0 < y) :
theorem
sub_floor_div_mul_lt
{α : Type u_1}
[linear_ordered_field α]
[floor_ring α]
(x : α)
{y : α}
(hy : 0 < y) :
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
- archimedean.floor_ring α = {floor := λ (x : α), classical.some _, le_floor := _}
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
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_btwn
{α : Type u_1}
[linear_ordered_field α]
[archimedean α]
{x y : α}
(h : x < y) :
theorem
exists_nat_one_div_lt
{α : Type u_1}
[linear_ordered_field α]
[archimedean α]
{ε : α}
(hε : 0 < ε) :
theorem
exists_pos_rat_lt
{α : Type u_1}
[linear_ordered_field α]
[archimedean α]
{x : α}
(x0 : 0 < x) :
@[simp]
theorem
exists_rat_near
{α : Type u_1}
[discrete_linear_ordered_field α]
[archimedean α]
(x : α)
{ε : α}
(ε0 : 0 < ε) :
@[simp]