mathlib documentation


Conditionally complete linear ordered fields #

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 #

Main results #

References #

Tags #

reals, conditionally complete, ordered field, uniqueness

structure conditionally_complete_linear_ordered_field (α : Type u_5) :
Type u_5

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.


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) [linear_ordered_field α] [division_ring β] (a : α) :
set β

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

theorem linear_ordered_field.cut_map_mono {α : Type u_2} (β : Type u_3) [linear_ordered_field α] [division_ring β] {a₁ a₂ : α} (h : a₁ a₂) :
theorem linear_ordered_field.mem_cut_map_iff {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [division_ring β] {a : α} {b : β} :
b linear_ordered_field.cut_map β a ∃ (q : ), q < a q = b
theorem linear_ordered_field.coe_mem_cut_map_iff {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [division_ring β] {a : α} {q : } [char_zero β] :
theorem linear_ordered_field.cut_map_coe {α : Type u_2} (β : Type u_3) [linear_ordered_field α] [linear_ordered_field β] (q : ) :

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) [linear_ordered_field α] [conditionally_complete_linear_ordered_field β] (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.

theorem linear_ordered_field.lt_induced_map_iff {α : Type u_2} {β : Type u_3} [linear_ordered_field α] [conditionally_complete_linear_ordered_field β] [archimedean α] {a : α} {b : β} :
b < linear_ordered_field.induced_map α β a ∃ (q : ), b < q q < a

Preparatory lemma for induced_ring_hom.

Preparatory lemma for induced_ring_hom.

induced_map as an additive homomorphism.


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

@[protected, instance]

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

@[protected, instance]

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

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

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