Topic: characterisation of reals
Kevin Buzzard (Nov 17 2018 at 08:32):
import algebra.archimedean import data.real.basic -- non-empty and bounded -> LUB definition is_complete (k : Type*) [has_le k] : Prop := ∀ (S : set k), (∃ x, x ∈ S) → (∃ x, ∀ y ∈ S, y ≤ x) → ∃ x, ∀ y, x ≤ y ↔ ∀ z ∈ S, z ≤ y -- this is already in Lean theorem real.complete : is_complete ℝ := λ S, real.exists_sup S -- have I got this right? theorem characterisation_of_reals_first_attempt (k : Type*) [linear_ordered_field k] [archimedean k] : is_complete k → ∃ f : k → ℝ, function.bijective f ∧ is_ring_hom f := sorry
I remember talking about this sort of thing with Patrick and others several months ago. I was teaching this stuff recently and I meant to get around to looking at this, but we ended up doing constructions of the reals via Dedekind cuts and Cauchy sequences and proving basic stuff like existence of floor function and density of rationals in reals from the completeness axiom instead.
Is this already in mathlib?
Last updated: May 06 2021 at 18:20 UTC