Documentation

Mathlib.Data.Real.Embedding

Embedding of archimedean groups into reals #

This file provides embedding of any archimedean groups into reals.

Main declarations #

theorem mul_smul_one_lt_iff {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {num : } {n den : } (hn : 0 < n) {x : M} :
(num * n) 1 < (n * den) x num 1 < den x
theorem num_smul_one_lt_den_smul_add {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {u v : } {x y : M} (hu : u.num 1 < u.den x) (hv : v.num 1 < v.den y) :
(u + v).num 1 < (u + v).den (x + y)

For u v : ℚ and x y : M, one can informally write u < x → v < y → u + v < x + y. We formalize this using smul.

theorem num_le_nat_mul_den {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] [ZeroLEOneClass M] [NeZero 1] {num : } {den : } {x : M} (h : num 1 den x) {n : } (hn : x n 1) :
num n * den

Given x from M, one can informally write that, by transitivity, num / den ≤ x → x ≤ n → num / den ≤ n for den : ℕ and num n : ℕ. To avoid writing division for integer num and den, we express this in terms of multiplication.

@[reducible, inline]
abbrev Archimedean.ratLt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) :

Set of rational numbers that are less than the "number" x / 1. Formally, these are numbers p / q such that p • 1 < q • x.

Equations
Instances For
    theorem Archimedean.mkRat_mem_ratLt {M : Type u_1} [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [One M] {num : } {den : } (hden : den 0) {x : M} :
    mkRat num den ratLt x num 1 < den x
    @[reducible, inline]
    abbrev Archimedean.ratLt' {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) :

    ratLt as a set of real numbers.

    Equations
    Instances For
      @[reducible, inline]
      noncomputable abbrev Archimedean.embedRealFun {M : Type u_1} [AddCommGroup M] [LinearOrder M] [One M] (x : M) :

      Mapping M to , defined as the supremum of ratLt' x.

      Equations
      Instances For

        The bundled M →+o ℝ for archimedean M that preserves 1.

        Equations
        Instances For