Definitions of Archimedean monoids

This file defines the archimedean property for ordered monoids.

Main definitions

• Archimedean is a typeclass for an ordered additive commutative monoid to have the archimedean property.
• MulArchimedean is a typeclass for an ordered commutative monoid to have the "mul-archimedean property" where for x and y > 1, there exists a natural number n such that x ≤ y ^ n.

class Archimedean (R : Type u_2) [AddCommMonoid R] [PartialOrder R] : Prop

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.

• arch (x : R) {y : R} : 0 < y → ∃ (n : ℕ), x ≤ n • y

  For any two elements x, y such that 0 < y, there exists a natural number n such that x ≤ n • y.

class MulArchimedean (R : Type u_2) [CommMonoid R] [PartialOrder R] : Prop

An ordered commutative monoid is called MulArchimedean if for any two elements x, y such that 1 < y, there exists a natural number n such that x ≤ y ^ n.

• arch (x : R) {y : R} : 1 < y → ∃ (n : ℕ), x ≤ y ^ n

  For any two elements x, y such that 1 < y, there exists a natural number n such that x ≤ y ^ n.

theorem exists_lt_pow {R : Type u_1} [CommMonoid R] [PartialOrder R] [MulLeftStrictMono R] [MulArchimedean R] {a : R} (ha : 1 < a) (b : R) : ∃ (n : ℕ), b < a ^ n

theorem exists_lt_nsmul {R : Type u_1} [AddCommMonoid R] [PartialOrder R] [AddLeftStrictMono R] [Archimedean R] {a : R} (ha : 0 < a) (b : R) : ∃ (n : ℕ), b < n • a

theorem exists_pow_lt {R : Type u_1} [CommGroup R] [LinearOrder R] [IsOrderedMonoid R] [MulArchimedean R] {a : R} (ha : a < 1) (b : R) : ∃ (n : ℕ), a ^ n < b

theorem exists_nsmul_lt {R : Type u_1} [AddCommGroup R] [LinearOrder R] [IsOrderedAddMonoid R] [Archimedean R] {a : R} (ha : a < 0) (b : R) : ∃ (n : ℕ), n • a < b

theorem exists_nat_ge {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℕ), x ≤ ↑n

theorem exists_nat_gt {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℕ), x < ↑n

theorem exists_int_ge {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), x ≤ ↑n

theorem exists_int_le {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), ↑n ≤ x

theorem exists_int_gt {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), x < ↑n

theorem exists_int_lt {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) : ∃ (n : ℤ), ↑n < x