Analysis I, Section 4.3

I have attempted to make the translation as faithful a paraphrasing as possible of the original text. When there is a choice between a more idiomatic Lean solution and a more faithful translation, I have generally chosen the latter. In particular, there will be places where the Lean code could be "golfed" to be more elegant and idiomatic, but I have consciously avoided doing so.

Main constructions and results of this section:

Basic properties of absolute value and exponentiation on the rational numbers (here we use the Mathlib rational numbers ℚ rather than the Section 4.2 rational numbers).

Note: to avoid notational conflict, we are using the standard Mathlib definitions of absolute value and exponentiation. As such, it is possible to solve several of the exercises here rather easily using the Mathlib API for these operations. However, the spirit of the exercises is to solve these instead using the API provided in this section, as well as more basic Mathlib API for the rational numbers that does not reference either absolute value or exponentiation.

This definition needs to be made outside of the Section 4.3 namespace for technical reasons.

def Rat.close (ε : ℚ) (x y:ℚ) := |x-y| ≤ εnamespace Section_4_3

Definition 4.3.1 (Absolute value)

abbrev abs (x:ℚ) : ℚ := if x > 0 then x else (if x < 0 then -x else 0)theorem abs_of_pos {x: ℚ} (hx: x > 0) : abs x = x := byx:ℚhx:x > 0⊢ abs x = x simp [hx]All goals completed! 🐙

Definition 4.3.1 (Absolute value)

theorem abs_of_neg {x: ℚ} (hx: x < 0) : abs x = -x := byx:ℚhx:x < 0⊢ abs x = -x
  simp [abs, hx]x:ℚhx:x < 0⊢ 0 < x → x = -x
  intro hx'x:ℚhx:x < 0hx':0 < x⊢ x = -x
  linarithAll goals completed! 🐙

Definition 4.3.1 (Absolute value)

theorem abs_of_zero : abs 0 = 0 := by⊢ abs 0 = 0 rflAll goals completed! 🐙

(Not from textbook) This definition of absolute value agrees with the Mathlib one. Henceforth we use the Mathlib absolute value.

theorem declaration uses 'sorry'abs_eq_abs (x: ℚ) : abs x = |x| := byx:ℚ⊢ abs x = |x|
  sorryAll goals completed! 🐙

abbrev dist (x y : ℚ) := |x - y|

Definition 4.2 (Distance). We avoid the Mathlib notion of distance here because it is real-valued.

theorem dist_eq (x y: ℚ) : dist x y = |x-y| := rfl

Proposition 4.3.3(a) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_nonneg (x: ℚ) : |x| ≥ 0 := byx:ℚ⊢ |x| ≥ 0 sorryAll goals completed! 🐙

Proposition 4.3.3(a) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_eq_zero_iff (x: ℚ) : |x| = 0 ↔ x = 0 := byx:ℚ⊢ |x| = 0 ↔ x = 0 sorryAll goals completed! 🐙

Proposition 4.3.3(b) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_add (x y:ℚ) : |x + y| ≤ |x| + |y| := byx:ℚy:ℚ⊢ |x + y| ≤ |x| + |y| sorryAll goals completed! 🐙

Proposition 4.3.3(c) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_le_iff (x y:ℚ) : -y ≤ x ∧ x ≤ y ↔ |x| ≤ y  := byx:ℚy:ℚ⊢ -y ≤ x ∧ x ≤ y ↔ |x| ≤ y sorryAll goals completed! 🐙

Proposition 4.3.3(c) / Exercise 4.3.1

theorem declaration uses 'sorry'le_abs (x:ℚ) : -|x| ≤ x ∧ x ≤ |x|  := byx:ℚ⊢ -|x| ≤ x ∧ x ≤ |x| sorryAll goals completed! 🐙

Proposition 4.3.3(d) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_mul (x y:ℚ) : |x * y| = |x| * |y| := byx:ℚy:ℚ⊢ |x * y| = |x| * |y| sorryAll goals completed! 🐙

Proposition 4.3.3(d) / Exercise 4.3.1

theorem declaration uses 'sorry'abs_neg (x:ℚ) : |-x| = |x| := byx:ℚ⊢ |(-x)| = |x| sorryAll goals completed! 🐙

Proposition 4.3.3(e) / Exercise 4.3.1

theorem declaration uses 'sorry'dist_nonneg (x y:ℚ) : dist x y ≥ 0 := byx:ℚy:ℚ⊢ dist x y ≥ 0 sorryAll goals completed! 🐙

Proposition 4.3.3(e) / Exercise 4.3.1

theorem declaration uses 'sorry'dist_eq_zero_iff (x y:ℚ) : dist x y = 0 ↔ x = y := byx:ℚy:ℚ⊢ dist x y = 0 ↔ x = y
  sorryAll goals completed! 🐙

Proposition 4.3.3(f) / Exercise 4.3.1

theorem declaration uses 'sorry'dist_symm (x y:ℚ) : dist x y = dist y x := byx:ℚy:ℚ⊢ dist x y = dist y x sorryAll goals completed! 🐙

Proposition 4.3.3(f) / Exercise 4.3.1

theorem declaration uses 'sorry'dist_le (x y z:ℚ) : dist x z ≤ dist x y + dist y z := byx:ℚy:ℚz:ℚ⊢ dist x z ≤ dist x y + dist y z sorryAll goals completed! 🐙

Definition 4.3.4 (eps-closeness). In the text the notion is undefined for ε zero or negative, but it is more convenient in Lean to assign a "junk" definition in this case. But this also allows some relaxations of hypotheses in the lemmas that follow.

theorem close_iff (ε x y:ℚ): ε.close x y ↔ |x - y| ≤ ε := byε:ℚx:ℚy:ℚ⊢ ε.close x y ↔ |x - y| ≤ ε rflAll goals completed! 🐙

Examples 4.3.6

declaration uses 'sorry'example : (0.1:ℚ).close (0.99:ℚ) (1.01:ℚ) := by⊢ Rat.close 0.1 0.99 1.01 sorryAll goals completed! 🐙

Examples 4.3.6

declaration uses 'sorry'example : ¬ (0.01:ℚ).close (0.99:ℚ) (1.01:ℚ) := by⊢ ¬Rat.close 1e-2 0.99 1.01 sorryAll goals completed! 🐙

Examples 4.3.6

declaration uses 'sorry'example (ε : ℚ) (hε : ε > 0) : ε.close 2 2 := byε:ℚhε:ε > 0⊢ ε.close 2 2 sorryAll goals completed! 🐙

theorem declaration uses 'sorry'close_refl (x:ℚ) : (0:ℚ).close x x := byx:ℚ⊢ Rat.close 0 x x sorryAll goals completed! 🐙

Proposition 4.3.7(a) / Exercise 4.3.2

theorem declaration uses 'sorry'eq_if_close (x y:ℚ) : x = y ↔ ∀ ε:ℚ, ε > 0 → ε.close x y := byx:ℚy:ℚ⊢ x = y ↔ ∀ ε > 0, ε.close x y sorryAll goals completed! 🐙

Proposition 4.3.7(b) / Exercise 4.3.2

theorem declaration uses 'sorry'close_symm (ε x y:ℚ) : ε.close x y ↔ ε.close y x := byε:ℚx:ℚy:ℚ⊢ ε.close x y ↔ ε.close y x sorryAll goals completed! 🐙

Proposition 4.3.7(c) / Exercise 4.3.2

theorem declaration uses 'sorry'close_trans {ε δ x y:ℚ} (hxy: ε.close x y) (hyz: δ.close y z) : (ε + δ).close x z := byz:ℚε:ℚδ:ℚx:ℚy:ℚhxy:ε.close x yhyz:δ.close y z⊢ (ε + δ).close x z sorryAll goals completed! 🐙

Proposition 4.3.7(d) / Exercise 4.3.2

theorem declaration uses 'sorry'add_close {ε δ x y z w:ℚ} (hxy: ε.close x y) (hzw: δ.close z w) : (ε + δ).close (x+z) (y+w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.close x yhzw:δ.close z w⊢ (ε + δ).close (x + z) (y + w) sorryAll goals completed! 🐙

Proposition 4.3.7(d) / Exercise 4.3.2

theorem declaration uses 'sorry'sub_close {ε δ x y z w:ℚ} (hxy: ε.close x y) (hzw: δ.close z w) : (ε + δ).close (x-z) (y-w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.close x yhzw:δ.close z w⊢ (ε + δ).close (x - z) (y - w) sorryAll goals completed! 🐙

Proposition 4.3.7(e) / Exercise 4.3.2, slightly strengthened

theorem declaration uses 'sorry'close_mono {ε ε' x y:ℚ} (hxy: ε.close x y) (hε: ε' ≥  ε) : ε'.close x y := byε:ℚε':ℚx:ℚy:ℚhxy:ε.close x yhε:ε' ≥ ε⊢ ε'.close x y sorryAll goals completed! 🐙

Proposition 4.3.7(f) / Exercise 4.3.2

theorem declaration uses 'sorry'close_between {ε x y z w:ℚ} (hxy: ε.close x y) (hyz: ε.close x z) (hbetween: (y ≤ w ∧ w ≤ z) ∨ (z ≤ w ∧ w ≤ y)) : ε.close x w := byε:ℚx:ℚy:ℚz:ℚw:ℚhxy:ε.close x yhyz:ε.close x zhbetween:y ≤ w ∧ w ≤ z ∨ z ≤ w ∧ w ≤ y⊢ ε.close x w sorryAll goals completed! 🐙

Proposition 4.3.7(g) / Exercise 4.3.2

theorem declaration uses 'sorry'close_mul_right {ε x y z:ℚ} (hε: ε ≥ 0) (hxy: ε.close x y) : (ε*|z|).close (x * z) (y * z) := byε:ℚx:ℚy:ℚz:ℚhε:ε ≥ 0hxy:ε.close x y⊢ (ε * |z|).close (x * z) (y * z) sorryAll goals completed! 🐙

Proposition 4.3.7(h) / Exercise 4.3.2

theorem close_mul_mul {ε δ x y z w:ℚ} (hε: ε ≥ 0) (hxy: ε.close x y) (hzw: δ.close z w) : (ε*|z|+δ*|x|+ε*δ).close (x * z) (y * w) := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w)
  -- The proof is written to follow the structure of the original text, though on formalization it was revealed that the hypothesis δ ≥ 0 was unnecessary.
  set a := y-xε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - x⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w)
  have ha : y = x + a := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) simp [a]All goals completed! 🐙
  have haε: |a| ≤ ε := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) rwa [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:|y - x| ≤ εhzw:δ.close z wa:ℚ := y - xha:y = x + a⊢ |a| ≤ ε at hxy
  set b := w-zε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - z⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w)
  have hb : w = z + b := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) simp [b]All goals completed! 🐙
  have hbδ: |b| ≤ δ := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) rwa [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:|w - z| ≤ δa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + b⊢ |b| ≤ δ at hzw
  have : y*w = x * z + a * z + x * b + a * b := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z w⊢ (ε * |z| + δ * |x| + ε * δ).close (x * z) (y * w) rw [ha, hb]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δ⊢ (x + a) * (z + b) = x * z + a * z + x * b + a * b; ringAll goals completed! 🐙
  rw [close_symm, close_iff]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |y * w - x * z| ≤ ε * |z| + δ * |x| + ε * δ
  calc
    _ = |a * z + b * x + a * b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |y * w - x * z| = |a * z + b * x + a * b| rw [this]ε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |x * z + a * z + x * b + a * b - x * z| = |a * z + b * x + a * b|; congre_aε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ x * z + a * z + x * b + a * b - x * z = a * z + b * x + a * b; ringAll goals completed! 🐙
    _ ≤ |a * z + b * x| + |a * b| := abs_add _ _
    _ ≤ |a * z| + |b * x| + |a * b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |a * z + b * x| + |a * b| ≤ |a * z| + |b * x| + |a * b|
      gcongrbcε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |a * z + b * x| ≤ |a * z| + |b * x|; exact abs_add _ _All goals completed! 🐙
    _ = |a| * |z| + |b| * |x| + |a| * |b| := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |a * z| + |b * x| + |a * b| = |a| * |z| + |b| * |x| + |a| * |b|
      simp_rw [abs_mul]All goals completed! 🐙
    _ ≤ _ := byε:ℚδ:ℚx:ℚy:ℚz:ℚw:ℚhε:ε ≥ 0hxy:ε.close x yhzw:δ.close z wa:ℚ := y - xha:y = x + ahaε:|a| ≤ εb:ℚ := w - zhb:w = z + bhbδ:|b| ≤ δthis:y * w = x * z + a * z + x * b + a * b⊢ |a| * |z| + |b| * |x| + |a| * |b| ≤ ε * |z| + δ * |x| + ε * δ
      gcongrAll goals completed! 🐙

/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition.-/
lemma pow_zero (x:ℚ) : x^0 = 1 := rfl

example : (0:ℚ)^0 = 1 := pow_zero 0

/-- Definition 4.3.9 (exponentiation).  Here we use the Mathlib definition.-/
lemma pow_succ (x:ℚ) (n:ℕ) : x^(n+1) = x^n * x := _root_.pow_succ x n

Proposition 4.3.10 (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_add (x:ℚ) (m n:ℕ) : x^n * x^m = x^(n+m) := byx:ℚm:ℕn:ℕ⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_mul (x:ℚ) (m n:ℕ) : (x^n)^m = x^(n*m) := byx:ℚm:ℕn:ℕ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Proposition 4.3.10(a) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'mul_pow (x y:ℚ) (n:ℕ) : (x*y)^n = x^n * y^n := byx:ℚy:ℚn:ℕ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Proposition 4.3.10(b) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_eq_zero (x:ℚ) (n:ℕ) : x^n = 0 ↔ x = 0 := byx:ℚn:ℕ⊢ x ^ n = 0 ↔ x = 0 sorryAll goals completed! 🐙

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_nonneg {x:ℚ} (n:ℕ) (hx: x ≥ 0) : x^n ≥ 0 := byx:ℚn:ℕhx:x ≥ 0⊢ x ^ n ≥ 0 sorryAll goals completed! 🐙

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_pos {x:ℚ} (n:ℕ) (hx: x > 0) : x^n > 0 := byx:ℚn:ℕhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_ge_pow (x y:ℚ) (n:ℕ) (hxy: x ≥ y) (hy: y ≥ 0) : x^n ≥ y^n := byx:ℚy:ℚn:ℕhxy:x ≥ yhy:y ≥ 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

Proposition 4.3.10(c) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_gt_pow (x y:ℚ) (n:ℕ) (hxy: x > y) (hy: y ≥ 0) (hn: n > 0) : x^n > y^n := byx:ℚy:ℚn:ℕhxy:x > yhy:y ≥ 0hn:n > 0⊢ x ^ n > y ^ n sorryAll goals completed! 🐙

Proposition 4.3.10(d) (Properties of exponentiation, I) / Exercise 4.3.3

theorem declaration uses 'sorry'pow_abs (x:ℚ) (n:ℕ) : |x|^n = |x^n| := byx:ℚn:ℕ⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Definition 4.3.11 (Exponentiation to a negative number). Here we use the Mathlib notion of integer exponentiation

theorem zpow_neg (x:ℚ) (n:ℕ) : x^(-(n:ℤ)) = 1/(x^n) := byx:ℚn:ℕ⊢ x ^ (-↑n) = 1 / x ^ n simp only [ne_eq, _root_.zpow_neg, zpow_natCast, one_div]All goals completed! 🐙

example (x:ℚ): x^(-3:ℤ) = 1/(x^3) := zpow_neg x 3

example (x:ℚ): x^(-3:ℤ) = 1/(x*x*x) := byx:ℚ⊢ x ^ (-3) = 1 / (x * x * x)
  convert zpow_neg x 3h.e'_3.h.e'_6x:ℚ⊢ x * x * x = x ^ 3; ringAll goals completed! 🐙

theorem pow_eq_zpow (x:ℚ) (n:ℕ): x^(n:ℤ) = x^n := zpow_natCast x n

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_add (x:ℚ) (n m:ℤ) : x^n * x^m = x^(n+m) := byx:ℚn:ℤm:ℤ⊢ x ^ n * x ^ m = x ^ (n + m) sorryAll goals completed! 🐙

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_mul (x:ℚ) (n m:ℤ) : (x^n)^m = x^(n*m) := byx:ℚn:ℤm:ℤ⊢ (x ^ n) ^ m = x ^ (n * m) sorryAll goals completed! 🐙

Proposition 4.3.12(a) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'mul_zpow (x y:ℚ) (n:ℤ) : (x*y)^n = x^n * y^n := byx:ℚy:ℚn:ℤ⊢ (x * y) ^ n = x ^ n * y ^ n sorryAll goals completed! 🐙

Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_pos {x:ℚ} (n:ℤ) (hx: x > 0) : x^n > 0 := byx:ℚn:ℤhx:x > 0⊢ x ^ n > 0 sorryAll goals completed! 🐙

Proposition 4.3.12(b) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_ge_zpow {x y:ℚ} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n > 0): x^n ≥ y^n := byx:ℚy:ℚn:ℤhxy:x ≥ yhy:y > 0hn:n > 0⊢ x ^ n ≥ y ^ n sorryAll goals completed! 🐙

theorem declaration uses 'sorry'zpow_ge_zpow_ofneg {x y:ℚ} {n:ℤ} (hxy: x ≥ y) (hy: y > 0) (hn: n < 0) : x^n ≤ y^n := byx:ℚy:ℚn:ℤhxy:x ≥ yhy:y > 0hn:n < 0⊢ x ^ n ≤ y ^ n sorryAll goals completed! 🐙

Proposition 4.3.12(c) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_inj {x y:ℚ} {n:ℤ} (hx: x > 0) (hy : y > 0) (hn: n ≠ 0) (hxy: x^n = y^n) : x = y := byx:ℚy:ℚn:ℤhx:x > 0hy:y > 0hn:n ≠ 0hxy:x ^ n = y ^ n⊢ x = y sorryAll goals completed! 🐙

Proposition 4.3.12(d) (Properties of exponentiation, II) / Exercise 4.3.4

theorem declaration uses 'sorry'zpow_abs (x:ℚ) (n:ℤ) (hx: x ≠ 0) : |x|^n = |x^n| := byx:ℚn:ℤhx:x ≠ 0⊢ |x| ^ n = |x ^ n| sorryAll goals completed! 🐙

Exercise 4.3.5

theorem declaration uses 'sorry'two_pow_geq (N:ℕ) : 2^N ≥ N := byN:ℕ⊢ 2 ^ N ≥ N sorryAll goals completed! 🐙