Archimedean groups and fields. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines the archimedean property for ordered groups and proves several results connected to this notion. Being archimedean means that for all elements x and y>0 there exists a natural number n such that x ≤ n • y.

Main definitions #

archimedean is a typeclass for an ordered additive commutative monoid to have the archimedean property.
archimedean.floor_ring defines a floor function on an archimedean linearly ordered ring making it into a floor_ring.

Main statements #

ℕ, ℤ, and ℚ are archimedean.

source

@[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 of this typeclass

source

@[protected, instance]

def order_dual.archimedean {α : Type u_1} [ordered_add_comm_group α] [archimedean α] :

archimedean αᵒᵈ

source

theorem exists_unique_zsmul_near_of_pos {α : Type u_1} [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.

source

theorem exists_unique_zsmul_near_of_pos' {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (g : α) :

∃! (k : ℤ), 0 ≤ g - k • a ∧ g - k • a < a

source

theorem exists_unique_sub_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :

∃! (m : ℤ), b - m • a ∈ set.Ico c (c + a)

source

theorem exists_unique_add_zsmul_mem_Ico {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :

∃! (m : ℤ), b + m • a ∈ set.Ico c (c + a)

source

theorem exists_unique_add_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :

∃! (m : ℤ), b + m • a ∈ set.Ioc c (c + a)

source

theorem exists_unique_sub_zsmul_mem_Ioc {α : Type u_1} [linear_ordered_add_comm_group α] [archimedean α] {a : α} (ha : 0 < a) (b c : α) :

∃! (m : ℤ), b - m • a ∈ set.Ioc c (c + a)

source

theorem exists_nat_gt {α : Type u_1} [strict_ordered_semiring α] [archimedean α] (x : α) :

∃ (n : ℕ), x < ↑n

source

theorem exists_nat_ge {α : Type u_1} [strict_ordered_semiring α] [archimedean α] (x : α) :

∃ (n : ℕ), x ≤ ↑n

source

theorem add_one_pow_unbounded_of_pos {α : Type u_1} [strict_ordered_semiring α] [archimedean α] (x : α) {y : α} (hy : 0 < y) :

∃ (n : ℕ), x < (y + 1) ^ n

source

theorem pow_unbounded_of_one_lt {α : Type u_1} [strict_ordered_ring α] [archimedean α] (x : α) {y : α} (hy1 : 1 < y) :

∃ (n : ℕ), x < y ^ n

source

theorem exists_int_gt {α : Type u_1} [strict_ordered_ring α] [archimedean α] (x : α) :

∃ (n : ℤ), x < ↑n

source

theorem exists_int_lt {α : Type u_1} [strict_ordered_ring α] [archimedean α] (x : α) :

∃ (n : ℤ), ↑n < x

source

theorem exists_floor {α : Type u_1} [strict_ordered_ring α] [archimedean α] (x : α) :

∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ ↑z ≤ x

source

theorem exists_nat_pow_near {α : Type u_1} [linear_ordered_ring α] [archimedean α] {x y : α} (hx : 1 ≤ x) (hy : 1 < 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.

source

theorem exists_mem_Ico_zpow {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (hx : 0 < x) (hy : 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.

source

theorem exists_mem_Ioc_zpow {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (hx : 0 < x) (hy : 1 < y) :

∃ (n : ℤ), x ∈ set.Ioc (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_Ico_zpow, but with ≤ and < the other way around.

source

theorem exists_pow_lt_of_lt_one {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (hx : 0 < x) (hy : y < 1) :

∃ (n : ℕ), y ^ n < x

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

source

theorem exists_nat_pow_near_of_lt_one {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (xpos : 0 < x) (hx : x ≤ 1) (ypos : 0 < y) (hy : y < 1) :

∃ (n : ℕ), y ^ (n + 1) < x ∧ x ≤ y ^ n

Given x and y between 0 and 1, x is between two successive powers of y. This is the same as exists_nat_pow_near, but for elements between 0 and 1

source

theorem exists_rat_gt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :

∃ (q : ℚ), x < ↑q

source

theorem exists_rat_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] (x : α) :

∃ (q : ℚ), ↑q < x

source

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

∃ (q : ℚ), x < ↑q ∧ ↑q < y

source

theorem le_of_forall_rat_lt_imp_le {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (h : ∀ (q : ℚ), ↑q < x → ↑q ≤ y) :

x ≤ y

source

theorem le_of_forall_lt_rat_imp_le {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (h : ∀ (q : ℚ), y < ↑q → x ≤ ↑q) :

x ≤ y

source

theorem eq_of_forall_rat_lt_iff_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (h : ∀ (q : ℚ), ↑q < x ↔ ↑q < y) :

x = y

source

theorem eq_of_forall_lt_rat_iff_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {x y : α} (h : ∀ (q : ℚ), x < ↑q ↔ y < ↑q) :

x = y

source

theorem exists_nat_one_div_lt {α : Type u_1} [linear_ordered_field α] [archimedean α] {ε : α} (hε : 0 < ε) :

∃ (n : ℕ), 1 / (↑n + 1) < ε

source

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

∃ (q : ℚ), 0 < q ∧ ↑q < x

source

theorem exists_rat_near {α : Type u_1} [linear_ordered_field α] [archimedean α] {ε : α} (x : α) (ε0 : 0 < ε) :

∃ (q : ℚ), |x - ↑q| < ε

source

theorem archimedean_iff_nat_lt {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (n : ℕ), x < ↑n

source

theorem archimedean_iff_nat_le {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (n : ℕ), x ≤ ↑n

source

theorem archimedean_iff_int_lt {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (n : ℤ), x < ↑n

source

theorem archimedean_iff_int_le {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (n : ℤ), x ≤ ↑n

source

theorem archimedean_iff_rat_lt {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (q : ℚ), x < ↑q

source

theorem archimedean_iff_rat_le {α : Type u_1} [linear_ordered_field α] :

archimedean α ↔ ∀ (x : α), ∃ (q : ℚ), x ≤ ↑q

source

@[protected, instance]

def nat.archimedean :

archimedean ℕ

source

@[protected, instance]

def int.archimedean :

archimedean ℤ

source

@[protected, instance]

def rat.archimedean :

archimedean ℚ

source

noncomputable def archimedean.floor_ring (α : Type u_1) [linear_ordered_ring α] [archimedean α] :

floor_ring α

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_ring.of_floor α (λ (a : α), classical.some _) _

source

@[protected, instance]

def floor_ring.archimedean (α : Type u_1) [linear_ordered_field α] [floor_ring α] :

archimedean α

A linear ordered field that is a floor ring is archimedean.