Documentation

Mathlib.Algebra.Order.Archimedean.Basic

Archimedean groups and fields. #

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 #

Main statements #

class Archimedean (α : Type u_2) [OrderedAddCommMonoid α] :

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 : α) {y : α}, 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
    theorem Archimedean.arch {α : Type u_2} :
    ∀ {inst : OrderedAddCommMonoid α} [self : Archimedean α] (x : α) {y : α}, 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 (α : Type u_2) [OrderedCommMonoid α] :

    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 : α) {y : α}, 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
      theorem MulArchimedean.arch {α : Type u_2} :
      ∀ {inst : OrderedCommMonoid α} [self : MulArchimedean α] (x : α) {y : α}, 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.

      Equations
      • =
      theorem exists_lt_nsmul {M : Type u_2} [OrderedAddCommMonoid M] [Archimedean M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] {a : M} (ha : 0 < a) (b : M) :
      ∃ (n : ), b < n a
      theorem exists_lt_pow {M : Type u_2} [OrderedCommMonoid M] [MulArchimedean M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] {a : M} (ha : 1 < a) (b : M) :
      ∃ (n : ), b < a ^ n
      theorem existsUnique_zsmul_near_of_pos {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (g : α) :
      ∃! k : , k a g g < (k + 1) a

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

      theorem existsUnique_zpow_near_of_one_lt {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (g : α) :
      ∃! k : , a ^ k g g < a ^ (k + 1)

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

      theorem existsUnique_zsmul_near_of_pos' {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (g : α) :
      ∃! k : , 0 g - k a g - k a < a
      theorem existsUnique_zpow_near_of_one_lt' {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (g : α) :
      ∃! k : , 1 g / a ^ k g / a ^ k < a
      theorem existsUnique_sub_zsmul_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b : α) (c : α) :
      ∃! m : , b - m a Set.Ico c (c + a)
      theorem existsUnique_div_zpow_mem_Ico {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b : α) (c : α) :
      ∃! m : , b / a ^ m Set.Ico c (c * a)
      theorem existsUnique_add_zsmul_mem_Ico {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b : α) (c : α) :
      ∃! m : , b + m a Set.Ico c (c + a)
      theorem existsUnique_mul_zpow_mem_Ico {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b : α) (c : α) :
      ∃! m : , b * a ^ m Set.Ico c (c * a)
      theorem existsUnique_add_zsmul_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b : α) (c : α) :
      ∃! m : , b + m a Set.Ioc c (c + a)
      theorem existsUnique_add_zpow_mem_Ioc {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b : α) (c : α) :
      ∃! m : , b * a ^ m Set.Ioc c (c * a)
      theorem existsUnique_sub_zsmul_mem_Ioc {α : Type u_1} [LinearOrderedAddCommGroup α] [Archimedean α] {a : α} (ha : 0 < a) (b : α) (c : α) :
      ∃! m : , b - m a Set.Ioc c (c + a)
      theorem existsUnique_sub_zpow_mem_Ioc {α : Type u_1} [LinearOrderedCommGroup α] [MulArchimedean α] {a : α} (ha : 1 < a) (b : α) (c : α) :
      ∃! m : , b / a ^ m Set.Ioc c (c * a)
      theorem exists_nat_ge {α : Type u_1} [OrderedSemiring α] [Archimedean α] (x : α) :
      ∃ (n : ), x n
      @[instance 100]
      instance instIsDirectedLeOfArchimedean {α : Type u_1} [OrderedSemiring α] [Archimedean α] :
      IsDirected α fun (x1 x2 : α) => x1 x2
      Equations
      • =
      theorem exists_nat_gt {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] (x : α) :
      ∃ (n : ), x < n
      theorem add_one_pow_unbounded_of_pos {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] {y : α} (x : α) (hy : 0 < y) :
      ∃ (n : ), x < (y + 1) ^ n
      theorem pow_unbounded_of_one_lt {α : Type u_1} [StrictOrderedSemiring α] [Archimedean α] {y : α} [ExistsAddOfLE α] (x : α) (hy1 : 1 < y) :
      ∃ (n : ), x < y ^ n
      theorem exists_int_gt {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) :
      ∃ (n : ), x < n
      theorem exists_int_lt {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) :
      ∃ (n : ), n < x
      theorem exists_floor {α : Type u_1} [StrictOrderedRing α] [Archimedean α] (x : α) :
      ∃ (fl : ), ∀ (z : ), z fl z x
      theorem exists_nat_pow_near {α : Type u_1} [LinearOrderedSemiring α] [Archimedean α] [ExistsAddOfLE α] {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.

      theorem exists_nat_one_div_lt {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {ε : α} (hε : 0 < ε) :
      ∃ (n : ), 1 / (n + 1) < ε
      theorem exists_mem_Ico_zpow {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x : α} {y : α} [ExistsAddOfLE α] (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.

      theorem exists_mem_Ioc_zpow {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x : α} {y : α} [ExistsAddOfLE α] (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.

      theorem exists_pow_lt_of_lt_one {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x : α} {y : α} [ExistsAddOfLE α] (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.

      theorem exists_nat_pow_near_of_lt_one {α : Type u_1} [LinearOrderedSemifield α] [Archimedean α] {x : α} {y : α} [ExistsAddOfLE α] (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

      theorem exists_rat_gt {α : Type u_1} [LinearOrderedField α] [Archimedean α] (x : α) :
      ∃ (q : ), x < q
      theorem exists_rat_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] (x : α) :
      ∃ (q : ), q < x
      theorem exists_rat_btwn {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} (h : x < y) :
      ∃ (q : ), x < q q < y
      theorem le_of_forall_rat_lt_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} (h : ∀ (q : ), q < xq y) :
      x y
      theorem le_of_forall_lt_rat_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} (h : ∀ (q : ), y < qx q) :
      x y
      theorem le_iff_forall_rat_lt_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} :
      x y ∀ (q : ), q < xq y
      theorem le_iff_forall_lt_rat_imp_le {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} :
      x y ∀ (q : ), y < qx q
      theorem eq_of_forall_rat_lt_iff_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} (h : ∀ (q : ), q < x q < y) :
      x = y
      theorem eq_of_forall_lt_rat_iff_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} {y : α} (h : ∀ (q : ), x < q y < q) :
      x = y
      theorem exists_pos_rat_lt {α : Type u_1} [LinearOrderedField α] [Archimedean α] {x : α} (x0 : 0 < x) :
      ∃ (q : ), 0 < q q < x
      theorem exists_rat_near {α : Type u_1} [LinearOrderedField α] [Archimedean α] {ε : α} (x : α) (ε0 : 0 < ε) :
      ∃ (q : ), |x - q| < ε
      theorem archimedean_iff_nat_lt {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (n : ), x < n
      theorem archimedean_iff_nat_le {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (n : ), x n
      theorem archimedean_iff_int_lt {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (n : ), x < n
      theorem archimedean_iff_int_le {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (n : ), x n
      theorem archimedean_iff_rat_lt {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (q : ), x < q
      theorem archimedean_iff_rat_le {α : Type u_1} [LinearOrderedField α] :
      Archimedean α ∀ (x : α), ∃ (q : ), x q
      instance Nonneg.instArchimedean {α : Type u_1} [OrderedAddCommMonoid α] [Archimedean α] :
      Archimedean { x : α // 0 x }
      Equations
      • =
      Equations
      • =
      noncomputable def Archimedean.floorRing (α : Type u_3) [LinearOrderedRing α] [Archimedean α] :

      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
      Instances For
        @[instance 100]

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

        Equations
        • =
        Equations
        • =