# mathlib3documentation

algebra.order.complete_field

# Conditionally complete linear ordered fields #

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

This file shows that the reals are unique, or, more formally, given a type satisfying the common axioms of the reals (field, conditionally complete, linearly ordered) that there is an isomorphism preserving these properties to the reals. This is rat.induced_order_ring_iso. Moreover this isomorphism is unique.

We introduce definitions of conditionally complete linear ordered fields, and show all such are archimedean. We also construct the natural map from a linear_ordered_field to such a field.

## Main definitions #

• conditionally_complete_linear_ordered_field: A field satisfying the standard axiomatization of the real numbers, being a Dedekind complete and linear ordered field.
• linear_ordered_field.induced_map: A (unique) map from any archimedean linear ordered field to a conditionally complete linear ordered field. Various bundlings are available.

## Main results #

• unique.order_ring_hom : Uniqueness of order_ring_homs from an archimedean linear ordered field to a conditionally complete linear ordered field.
• unique.order_ring_iso : Uniqueness of order_ring_isos between two conditionally complete linearly ordered fields.

## Tags #

reals, conditionally complete, ordered field, uniqueness

@[instance]
@[instance]
@[class]

A field which is both linearly ordered and conditionally complete with respect to the order. This axiomatizes the reals.

Instances of this typeclass
Instances of other typeclasses for conditionally_complete_linear_ordered_field
• conditionally_complete_linear_ordered_field.has_sizeof_inst
@[protected, instance]

Any conditionally complete linearly ordered field is archimedean.

@[protected, instance]

The reals are a conditionally complete linearly ordered field.

Equations

### Rational cut map #

The idea is that a conditionally complete linear ordered field is fully characterized by its copy of the rationals. Hence we define rat.cut_map β : α → set β which sends a : α to the "rationals in β" that are less than a.

def linear_ordered_field.cut_map {α : Type u_2} (β : Type u_3) (a : α) :
set β

The lower cut of rationals inside a linear ordered field that are less than a given element of another linear ordered field.

Equations
theorem linear_ordered_field.cut_map_mono {α : Type u_2} (β : Type u_3) {a₁ a₂ : α} (h : a₁ a₂) :
@[simp]
theorem linear_ordered_field.mem_cut_map_iff {α : Type u_2} {β : Type u_3} {a : α} {b : β} :
(q : ), q < a q = b
@[simp]
theorem linear_ordered_field.coe_mem_cut_map_iff {α : Type u_2} {β : Type u_3} {a : α} {q : } [char_zero β] :
q < a
theorem linear_ordered_field.cut_map_self {α : Type u_2} (a : α) :
theorem linear_ordered_field.cut_map_coe {α : Type u_2} (β : Type u_3) (q : ) :
= coe '' {r : | r < q}
theorem linear_ordered_field.cut_map_nonempty {α : Type u_2} (β : Type u_3) [archimedean α] (a : α) :
theorem linear_ordered_field.cut_map_bdd_above {α : Type u_2} (β : Type u_3) [archimedean α] (a : α) :
theorem linear_ordered_field.cut_map_add {α : Type u_2} (β : Type u_3) [archimedean α] (a b : α) :

### Induced map #

rat.cut_map spits out a set β. To get something in β, we now take the supremum.

def linear_ordered_field.induced_map (α : Type u_2) (β : Type u_3) (x : α) :
β

The induced order preserving function from a linear ordered field to a conditionally complete linear ordered field, defined by taking the Sup in the codomain of all the rationals less than the input.

Equations
theorem linear_ordered_field.induced_map_mono (α : Type u_2) (β : Type u_3) [archimedean α] :
theorem linear_ordered_field.induced_map_rat (α : Type u_2) (β : Type u_3) [archimedean α] (q : ) :
@[simp]
theorem linear_ordered_field.induced_map_zero (α : Type u_2) (β : Type u_3) [archimedean α] :
@[simp]
theorem linear_ordered_field.induced_map_one (α : Type u_2) (β : Type u_3) [archimedean α] :
theorem linear_ordered_field.induced_map_nonneg {α : Type u_2} {β : Type u_3} [archimedean α] {a : α} (ha : 0 a) :
theorem linear_ordered_field.coe_lt_induced_map_iff {α : Type u_2} {β : Type u_3} [archimedean α] {a : α} {q : } :
q < a
theorem linear_ordered_field.lt_induced_map_iff {α : Type u_2} {β : Type u_3} [archimedean α] {a : α} {b : β} :
(q : ), b < q q < a
@[simp]
theorem linear_ordered_field.induced_map_self {β : Type u_3} (b : β) :
@[simp]
theorem linear_ordered_field.induced_map_induced_map (α : Type u_2) (β : Type u_3) (γ : Type u_4) [archimedean α] (a : α) :
@[simp]
theorem linear_ordered_field.induced_map_inv_self (β : Type u_3) (γ : Type u_4) (b : β) :
theorem linear_ordered_field.induced_map_add (α : Type u_2) (β : Type u_3) [archimedean α] (x y : α) :
(x + y) =
theorem linear_ordered_field.le_induced_map_mul_self_of_mem_cut_map {α : Type u_2} {β : Type u_3} [archimedean α] {a : α} (ha : 0 < a) (b : β) (hb : b (a * a)) :

Preparatory lemma for induced_ring_hom.

theorem linear_ordered_field.exists_mem_cut_map_mul_self_of_lt_induced_map_mul_self {α : Type u_2} {β : Type u_3} [archimedean α] {a : α} (ha : 0 < a) (b : β) (hba : b < ) :
(c : β) (H : c (a * a)), b < c

Preparatory lemma for induced_ring_hom.

def linear_ordered_field.induced_add_hom (α : Type u_2) (β : Type u_3) [archimedean α] :
α →+ β

induced_map as an additive homomorphism.

Equations
@[simp]
def linear_ordered_field.induced_order_ring_hom (α : Type u_2) (β : Type u_3) [archimedean α] :
α →+*o β

induced_map as an order_ring_hom.

Equations
def linear_ordered_field.induced_order_ring_iso (β : Type u_3) (γ : Type u_4)  :
β ≃+*o γ

The isomorphism of ordered rings between two conditionally complete linearly ordered fields.

Equations
@[simp]
@[simp]
@[simp]
@[protected, instance]
def linear_ordered_field.order_ring_hom.unique (α : Type u_2) (β : Type u_3) [archimedean α] :
unique →+*o β)

There is a unique ordered ring homomorphism from an archimedean linear ordered field to a conditionally complete linear ordered field.

Equations
@[protected, instance]
def linear_ordered_field.order_ring_iso.unique (β : Type u_3) (γ : Type u_4)  :
unique ≃+*o γ)

There is a unique ordered ring isomorphism between two conditionally complete linear ordered fields.

Equations
theorem ring_hom_monotone {R : Type u_5} {S : Type u_6} [ordered_ring R] (hR : (r : R), 0 r ( (s : R), s ^ 2 = r)) (f : R →+* S) :
@[protected, instance]

There exists no nontrivial ring homomorphism ℝ →+* ℝ.

Equations