Books.IntroductiontoRealAnalysisVolumeI_JiriLebl

theorem real_exists_complete_ordered_field :

∃ (R : Type) (hF : Field R) (hL : LinearOrder R) (hS : IsStrictOrderedRing R), let x := hF; let x_1 := hL; have x_2 := hS; (∀ {E : Set R}, E.Nonempty → BddAbove E → ∃ (supE : R), IsLUB E supE) ∧ Function.Injective fun (q : ℚ) => ↑q

Theorem 1.2.1: There exists an ordered field ℝ with the least-upper-bound property containing the rationals ℚ; such a structure is unique up to an order-preserving field isomorphism.

source

theorem real_unique_complete_ordered_field (R : Type u) [ConditionallyCompleteLinearOrderedField R] (S : Type v) [ConditionallyCompleteLinearOrderedField S] :

Nonempty (R ≃+* S)

Any two ordered fields with the least-upper-bound property that contain the rationals are isomorphic as ordered fields.

source

theorem real_le_zero_of_le_pos {x : ℝ} (h : ∀ ε > 0, x ≤ ε) :

x ≤ 0

Proposition 1.2.2: If a real number x satisfies x ≤ ε for every ε > 0, then x ≤ 0.

source

theorem exists_unique_pos_sq_eq_two :

∃! r : ℝ , 0 < r ∧ r ^ 2 = 2

Example 1.2.3: There exists a unique positive real number r such that r ^ 2 = 2; this number is denoted √2.

source

noncomputable def sqrtTwo :

ℝ

The book's notation √2 realized via the mathlib square root.

Equations

sqrtTwo = √2

Instances For

source

theorem sqrtTwo_spec :

0 < sqrtTwo ∧ sqrtTwo ^ 2 = 2

The element sqrtTwo is positive and squares to 2, matching the defining property of √2.

source

theorem sqrtTwo_unique {r : ℝ} (hr : 0 < r ∧ r ^ 2 = 2) :

r = sqrtTwo

Uniqueness of the positive square root of 2.

source

theorem archimedean_and_rat_dense :

(∀ (x y : ℝ), 0 < x → ∃ (n : ℕ), ↑n * x > y) ∧ ∀ (x y : ℝ), x < y → ∃ (r : ℚ), x < ↑r ∧ ↑r < y

Theorem 1.2.4: (i) (Archimedean property) If x, y ∈ ℝ with x > 0, then there exists n ∈ ℕ such that n * x > y. (ii) (ℚ is dense in ℝ) If x, y ∈ ℝ with x < y, then there exists r ∈ ℚ such that x < r < y.

source

theorem inf_nat_inv_eq_zero :

sInf (Set.range fun (n : ℕ) => 1 / ↑n.succ) = 0

Corollary 1.2.5: The infimum of the set {1 / n : n ∈ ℕ} is 0.

source

theorem sup_inf_arithmetic {A : Set ℝ} (hA : A.Nonempty) :

(∀ (x : ℝ), BddAbove A → sSup ((fun (a : ℝ) => x + a) '' A) = x + sSup A) ∧ (∀ (x : ℝ), BddBelow A → sInf ((fun (a : ℝ) => x + a) '' A) = x + sInf A) ∧ (∀ {x : ℝ}, 0 < x → BddAbove A → sSup ((fun (a : ℝ) => x * a) '' A) = x * sSup A) ∧ (∀ {x : ℝ}, 0 < x → BddBelow A → sInf ((fun (a : ℝ) => x * a) '' A) = x * sInf A) ∧ (∀ {x : ℝ}, x < 0 → BddBelow A → sSup ((fun (a : ℝ) => x * a) '' A) = x * sInf A) ∧ ∀ {x : ℝ}, x < 0 → BddAbove A → sInf ((fun (a : ℝ) => x * a) '' A) = x * sSup A

Proposition 1.2.6: Let A ⊆ ℝ be nonempty. (i) If A is bounded above, then sup (x + A) = x + sup A. (ii) If A is bounded below, then inf (x + A) = x + inf A. (iii) If x > 0 and A is bounded above, then sup (x * A) = x * sup A. (iv) If x > 0 and A is bounded below, then inf (x * A) = x * inf A. (v) If x < 0 and A is bounded below, then sup (x * A) = x * inf A. (vi) If x < 0 and A is bounded above, then inf (x * A) = x * sup A.

source

theorem sup_le_inf_of_forall_le {A B : Set ℝ} (hA : A.Nonempty) (hB : B.Nonempty) (h : ∀ x ∈ A, ∀ y ∈ B, x ≤ y) :

BddAbove A ∧ BddBelow B ∧ sSup A ≤ sInf B

Proposition 1.2.7: If nonempty sets A, B ⊆ ℝ satisfy x ≤ y whenever x ∈ A and y ∈ B, then A is bounded above, B is bounded below, and sSup A ≤ sInf B.

source

theorem exists_mem_between_sub_sup {S : Set ℝ} (hS : S.Nonempty) (hSb : BddAbove S) {ε : ℝ} (hε : 0 < ε) :

∃ x ∈ S, sSup S - ε < x ∧ x ≤ sSup S

Proposition 1.2.8: If S ⊆ ℝ is nonempty and bounded above, then for every ε > 0 there exists x ∈ S with sSup S - ε < x ≤ sSup S.

source

noncomputable def extendedSup (A : Set ℝ) :

EReal

Definition 1.2.9: For a subset A ⊆ ℝ, extend sup and inf to the extended reals so that (i) sup ∅ = -∞, (ii) if A is unbounded above then sup A = ∞, (iii) inf ∅ = ∞, and (iv) if A is unbounded below then inf A = -∞. These agree with sSup and sInf on EReal when we view A as a set of extended real numbers.