Documentation

Mathlib.Algebra.Order.Archimedean.Defs

Definitions of Archimedean monoids #

This file defines the archimedean property for ordered monoids.

Main definitions #

source
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.

Instances
    source
    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.

    Instances
      source
      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
      source
      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
      source
      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
      source
      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
      source
      theorem exists_nat_ge {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℕ), x ≤ ↑n
      source
      theorem exists_nat_gt {R : Type u_1} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℕ), x < ↑n
      source
      theorem exists_int_ge {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℤ), x ≤ ↑n
      source
      theorem exists_int_le {R : Type u_1} [Ring R] [PartialOrder R] [IsOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℤ), ↑n ≤ x
      source
      theorem exists_int_gt {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℤ), x < ↑n
      source
      theorem exists_int_lt {R : Type u_1} [Ring R] [PartialOrder R] [IsStrictOrderedRing R] [Archimedean R] (x : R) :
      ∃ (n : ℤ), ↑n < x