theorem RealNumbers.real_numbers_theorem : IsStrictOrderedRing ℝ ∧ Function.Injective Rat.cast ∧ ∀ (S : Set ℝ), S.Nonempty → BddAbove S → ∃ (x : ℝ), IsLUB S x

The real numbers ℝ form a strict ordered ring, contain ℚ via an injective ring homomorphism, and satisfy the least upper bound property: every nonempty set bounded above admits a least upper bound.

theorem RealNumbers.real_uniqueness_up_to_iso (F : Type u_1) [Field F] [LinearOrder F] [IsStrictOrderedRing F] [ConditionallyCompleteLinearOrder F] : Nonempty (F ≃+*o ℝ)

Uniqueness (up to ordered ring isomorphism) of the real numbers: any conditionally complete linear strict ordered field F is isomorphic to ℝ as an ordered ring.

theorem RealNumbers.sqrt2_exists_unique : ∃! r : ℝ, 0 < r ∧ r ^ 2 = 2

There exists a unique positive real number r with r ^ 2 = 2, namely √2; in particular √2 ∈ ℝ \ ℚ.