Аналіз I, Глава 6.2

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:

Some API for Mathlib's extended reals EReal : TypeEReal, particularly with regard to the supremum operation SupSet.sSup.{u_1} {α : Type u_1} [self : SupSet α] : Set α → αsSup and infimum operation InfSet.sInf.{u_1} {α : Type u_1} [self : InfSet α] : Set α → αsInf.

Визначення 6.2.1

theorem EReal.def (x:EReal) : (∃ (y:Real), y = x) ∨ x = ⊤ ∨ x = ⊥ := byx:EReal⊢ (∃ y, ↑y = x) ∨ x = ⊤ ∨ x = ⊥
  revert x⊢ ∀ (x : EReal), (∃ y, ↑y = x) ∨ x = ⊤ ∨ x = ⊥
  rw [EReal.forall]⊢ ((∃ y, ↑y = ⊥) ∨ ⊥ = ⊤ ∨ ⊥ = ⊥) ∧ ((∃ y, ↑y = ⊤) ∨ ⊤ = ⊤ ∨ ⊤ = ⊥) ∧ ∀ (r : ℝ), (∃ y, ↑y = ↑r) ∨ ↑r = ⊤ ∨ ↑r = ⊥
  simpAll goals completed! 🐙

theorem EReal.real_neq_infty (x:ℝ) : (x:EReal) ≠ ⊤ := coe_ne_top _theorem EReal.real_neq_neg_infty (x:ℝ) : (x:EReal) ≠ ⊥ := coe_ne_bot _theorem EReal.infty_neq_neg_infty : (⊤:EReal) ≠ (⊥:EReal) := add_top_iff_ne_bot.mp rflabbrev EReal.isFinite (x:EReal) : Prop := ∃ (y:Real), y = xabbrev EReal.isInfinite (x:EReal) : Prop := x = ⊤ ∨ x = ⊥

theorem EReal.infinite_iff_not_finite (x:EReal): x.isInfinite ↔ ¬ x.isFinite := byx:EReal⊢ x.isInfinite ↔ ¬x.isFinite
  unfold isFinite isInfinitex:EReal⊢ x = ⊤ ∨ x = ⊥ ↔ ¬∃ y, ↑y = x
  rcases EReal.def x with h | h | hinlx:ERealh:∃ y, ↑y = x⊢ x = ⊤ ∨ x = ⊥ ↔ ¬∃ y, ↑y = xinr.inlx:ERealh:x = ⊤⊢ x = ⊤ ∨ x = ⊥ ↔ ¬∃ y, ↑y = xinr.inrx:ERealh:x = ⊥⊢ x = ⊤ ∨ x = ⊥ ↔ ¬∃ y, ↑y = x
  all_goals simp [h]All goals completed! 🐙
  obtain ⟨ y, rfl ⟩ := hinl.introy:ℝ⊢ ¬↑y = ⊤ ∧ ¬↑y = ⊥
  simpAll goals completed! 🐙

Визначення 6.2.2 (Negation of extended reals)

theorem EReal.neg_of_real (x:Real) : -(x:EReal) = (-x:ℝ) := rfl

EReal.neg_top : -⊤ = ⊥#check EReal.neg_top

EReal.neg_top : -⊤ = ⊥

EReal.neg_bot : -⊥ = ⊤#check EReal.neg_bot

EReal.neg_bot : -⊥ = ⊤

Визначення 6.2.3 (Ordering of extended reals)

theorem EReal.le_iff (x y:EReal) :
    x ≤ y ↔ (∃ (x' y':Real), x = x' ∧ y = y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥ := byx:ERealy:EReal⊢ x ≤ y ↔ (∃ x' y', x = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥
  rcases EReal.def x with hx | rfl | rflinlx:ERealy:ERealhx:∃ y, ↑y = x⊢ x ≤ y ↔ (∃ x' y', x = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ x = ⊥inr.inly:EReal⊢ ⊤ ≤ y ↔ (∃ x' y', ⊤ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊤ = ⊥inr.inry:EReal⊢ ⊥ ≤ y ↔ (∃ x' y', ⊥ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊥ = ⊥
  all_goals rcases EReal.def y with hy | rfl | rflinr.inr.inly:ERealhy:∃ y_1, ↑y_1 = y⊢ ⊥ ≤ y ↔ (∃ x' y', ⊥ = ↑x' ∧ y = ↑y' ∧ x' ≤ y') ∨ y = ⊤ ∨ ⊥ = ⊥inr.inr.inr.inl⊢ ⊥ ≤ ⊤ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊤ = ↑y' ∧ x' ≤ y') ∨ ⊤ = ⊤ ∨ ⊥ = ⊥inr.inr.inr.inr⊢ ⊥ ≤ ⊥ ↔ (∃ x' y', ⊥ = ↑x' ∧ ⊥ = ↑y' ∧ x' ≤ y') ∨ ⊥ = ⊤ ∨ ⊥ = ⊥
  all_goals simpAll goals completed! 🐙
  obtain ⟨ x', rfl ⟩ := hxinl.inl.introy:ERealhy:∃ y_1, ↑y_1 = yx':ℝ⊢ ↑x' ≤ y ↔ (∃ x'_1, ↑x' = ↑x'_1 ∧ ∃ x, y = ↑x ∧ x'_1 ≤ x) ∨ y = ⊤ ∨ ↑x' = ⊥
  obtain ⟨ y', rfl ⟩ := hyinl.inl.intro.introx':ℝy':ℝ⊢ ↑x' ≤ ↑y' ↔ (∃ x'_1, ↑x' = ↑x'_1 ∧ ∃ x, ↑y' = ↑x ∧ x'_1 ≤ x) ∨ ↑y' = ⊤ ∨ ↑x' = ⊥
  simpAll goals completed! 🐙

Визначення 6.2.3 (Ordering of extended reals)

theorem EReal.lt_iff (x y:EReal) : x < y ↔ x ≤ y ∧ x ≠ y := lt_iff_le_and_ne

EReal.coe_lt_coe_iff {x y : ℝ} : ↑x < ↑y ↔ x < y#check EReal.coe_lt_coe_iff

EReal.coe_lt_coe_iff {x y : ℝ} : ↑x < ↑y ↔ x < y

Приклади 6.2.4

declaration uses 'sorry'example : (3:EReal) ≤ (5:EReal) := by⊢ 3 ≤ 5 sorryAll goals completed! 🐙

Приклади 6.2.4

declaration uses 'sorry'example : (3:EReal) < ⊤ := by⊢ 3 < ⊤ sorryAll goals completed! 🐙

Приклади 6.2.4

declaration uses 'sorry'example : (⊥:EReal) < ⊤ := by⊢ ⊥ < ⊤ sorryAll goals completed! 🐙

Приклади 6.2.4

declaration uses 'sorry'example : ¬ (3:EReal) ≤ ⊥ := by⊢ ¬3 ≤ ⊥ sorryAll goals completed! 🐙

instCompleteLinearOrderEReal : CompleteLinearOrder EReal#check instCompleteLinearOrderEReal

instCompleteLinearOrderEReal : CompleteLinearOrder EReal

Твердження 6.2.5(a) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.refl (x:EReal) : x ≤ x := byx:EReal⊢ x ≤ x sorryAll goals completed! 🐙

Твердження 6.2.5(b) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.trichotomy (x y:EReal) : x < y ∨ x = y ∨ x > y := byx:ERealy:EReal⊢ x < y ∨ x = y ∨ x > y sorryAll goals completed! 🐙

Твердження 6.2.5(b) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.not_lt_and_eq (x y:EReal) : ¬ (x < y ∧ x = y) := byx:ERealy:EReal⊢ ¬(x < y ∧ x = y) sorryAll goals completed! 🐙

Твердження 6.2.5(b) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.not_gt_and_eq (x y:EReal) : ¬ (x > y ∧ x = y) := byx:ERealy:EReal⊢ ¬(x > y ∧ x = y) sorryAll goals completed! 🐙

Твердження 6.2.5(b) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.not_lt_and_gt (x y:EReal) : ¬ (x < y ∧ x > y) := byx:ERealy:EReal⊢ ¬(x < y ∧ x > y) sorryAll goals completed! 🐙

Твердження 6.2.5(c) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.trans {x y z:EReal} (hxy : x ≤ y) (hyz: y ≤ z) : x ≤ z := byx:ERealy:ERealz:ERealhxy:x ≤ yhyz:y ≤ z⊢ x ≤ z sorryAll goals completed! 🐙

Твердження 6.2.5(d) / Вправа 6.2.1

theorem declaration uses 'sorry'EReal.neg_of_lt {x y:EReal} (hxy : x ≤ y): -y ≤ -x := byx:ERealy:ERealhxy:x ≤ y⊢ -y ≤ -x sorryAll goals completed! 🐙

Визначення 6.2.6

theorem EReal.sup_of_bounded_nonempty {E: Set ℝ} (hbound: BddAbove E) (hnon: E.Nonempty) :
    sSup ((fun (x:ℝ) ↦ (x:EReal)) '' E) = sSup E := calc
  _ = sSup
      ((fun (x:WithTop ℝ) ↦ (x:WithBot (WithTop ℝ))) '' ((fun (x:ℝ) ↦ (x:WithTop ℝ)) '' E)) := byE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E))
    rw [←Set.image_comp]E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = sSup (((fun x => ↑x) ∘ fun x => ↑x) '' E)
    congrAll goals completed! 🐙
  _ = sSup ((fun (x:ℝ) ↦ (x:WithTop ℝ)) '' E) := byE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E)) = ↑(sSup ((fun x => ↑x) '' E))
    symmE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup ((fun x => ↑x) '' E)) = sSup ((fun x => ↑x) '' ((fun x => ↑x) '' E))
    convert WithBot.coe_sSup' _ _convert_5E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ((fun x => ↑x) '' E).Nonemptyconvert_6E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ BddAbove ((fun x => ↑x) '' E)
    .convert_5E:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ((fun x => ↑x) '' E).Nonempty simp [hnon]All goals completed! 🐙
    exact Monotone.map_bddAbove WithTop.coe_mono hboundAll goals completed! 🐙
  _ = ((sSup E : ℝ) : WithTop ℝ) := byE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup ((fun x => ↑x) '' E)) = ↑↑(sSup E)
    congre_aE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = ↑(sSup E); symme_aE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑(sSup E) = sSup ((fun x => ↑x) '' E)
    exact WithTop.coe_sSup' hboundAll goals completed! 🐙
  _ = _ := byE:Set ℝhbound:BddAbove Ehnon:E.Nonempty⊢ ↑↑(sSup E) = ↑(sSup E) rflAll goals completed! 🐙

Визначення 6.2.6

theorem EReal.sup_of_unbounded_nonempty {E: Set ℝ} (hunbound: ¬ BddAbove E) (hnon: E.Nonempty) :
    sSup ((fun (x:ℝ) ↦ (x:EReal)) '' E) = ⊤ := byE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonempty⊢ sSup ((fun x => ↑x) '' E) = ⊤
  rw [sSup_eq_top]E:Set ℝhunbound:¬BddAbove Ehnon:E.Nonempty⊢ ∀ b < ⊤, ∃ a ∈ (fun x => ↑x) '' E, b < a
  intro b hbE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyb:ERealhb:b < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, b < a
  rcases EReal.def b with hb' | rfl | rflinlE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyb:ERealhb:b < ⊤hb':∃ y, ↑y = b⊢ ∃ a ∈ (fun x => ↑x) '' E, b < ainr.inlE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊤ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊤ < ainr.inrE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊥ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊥ < a
  .inlE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyb:ERealhb:b < ⊤hb':∃ y, ↑y = b⊢ ∃ a ∈ (fun x => ↑x) '' E, b < a obtain ⟨ y, rfl ⟩ := hb'inl.introE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyy:ℝhb:↑y < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ↑y < a
    simpinl.introE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyy:ℝhb:↑y < ⊤⊢ ∃ a ∈ E, y < a
    contrapose! hunboundinl.introE:Set ℝhnon:E.Nonemptyy:ℝhb:↑y < ⊤hunbound:∀ a ∈ E, a ≤ y⊢ BddAbove E
    exact ⟨ y, hunbound ⟩All goals completed! 🐙
  .inr.inlE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊤ < ⊤⊢ ∃ a ∈ (fun x => ↑x) '' E, ⊤ < a simp at hbAll goals completed! 🐙
  simpinr.inrE:Set ℝhunbound:¬BddAbove Ehnon:E.Nonemptyhb:⊥ < ⊤⊢ ∃ a, a ∈ E
  exact hnonAll goals completed! 🐙

Визначення 6.2.6

theorem EReal.sup_of_empty : sSup (∅:Set EReal) = ⊥ := sSup_empty

Визначення 6.2.6

theorem EReal.sup_of_infty_mem {E: Set EReal} (hE: ⊤ ∈ E) : sSup E = ⊤ := csSup_eq_top_of_top_mem hE

Визначення 6.2.6

theorem EReal.sup_of_neg_infty_mem {E: Set EReal} : sSup E = sSup (E \ {⊥}) :=
  (sSup_diff_singleton_bot _).symm

theorem EReal.inf_eq_neg_sup (E: Set EReal) : sInf E = - sSup (-E) := byE:Set EReal⊢ sInf E = -sSup (-E)
  simp_rw [←isGLB_iff_sInf_eq, isGLB_iff_le_iff, EReal.le_neg]E:Set EReal⊢ ∀ (b : EReal), sSup (-E) ≤ -b ↔ b ∈ lowerBounds E
  intro bE:Set ERealb:EReal⊢ sSup (-E) ≤ -b ↔ b ∈ lowerBounds E
  simp [lowerBounds]E:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) ↔ ∀ ⦃a : EReal⦄, a ∈ E → b ≤ a
  constructormpE:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) → ∀ ⦃a : EReal⦄, a ∈ E → b ≤ amprE:Set ERealb:EReal⊢ (∀ ⦃a : EReal⦄, a ∈ E → b ≤ a) → ∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b
  .mpE:Set ERealb:EReal⊢ (∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -b) → ∀ ⦃a : EReal⦄, a ∈ E → b ≤ a intro h a hampE:Set ERealb:ERealh:∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -ba:ERealha:a ∈ E⊢ b ≤ a
    specialize h (-a) (byE:Set ERealb:ERealh:∀ (b_1 : EReal), -b_1 ∈ E → b_1 ≤ -ba:ERealha:a ∈ E⊢ - -a ∈ E simp [ha]All goals completed! 🐙)
    exact neg_le_neg_iff.mp hAll goals completed! 🐙
  intro h a hamprE:Set ERealb:ERealh:∀ ⦃a : EReal⦄, a ∈ E → b ≤ aa:ERealha:-a ∈ E⊢ a ≤ -b
  specialize h hamprE:Set ERealb:EReala:ERealha:-a ∈ Eh:b ≤ -a⊢ a ≤ -b
  exact EReal.le_neg_of_le_neg hAll goals completed! 🐙

Приклад 6.2.7

abbrev Example_6_2_7 : Set EReal := { x | ∃ n:ℕ, x = -((n+1):EReal)} ∪ {⊥}

declaration uses 'sorry'example : sSup Example_6_2_7 = -1 := by⊢ sSup Example_6_2_7 = -1
  rw [EReal.sup_of_neg_infty_mem]⊢ sSup (Example_6_2_7 \ {⊥}) = -1
  sorryAll goals completed! 🐙

declaration uses 'sorry'example : sInf Example_6_2_7 = ⊥ := by⊢ sInf Example_6_2_7 = ⊥
  rw [EReal.inf_eq_neg_sup]⊢ -sSup (-Example_6_2_7) = ⊥
  sorryAll goals completed! 🐙

Приклад 6.2.8

abbrev Example_6_2_8 : Set EReal := { x | ∃ n:ℕ, x = (1 - (10:ℝ)^(-(n:ℤ)-1):Real)}

declaration uses 'sorry'example : sInf Example_6_2_8 = (0.9:ℝ) := by⊢ sInf Example_6_2_8 = ↑0.9 sorryAll goals completed! 🐙

declaration uses 'sorry'example : sSup Example_6_2_8 = 1 := by⊢ sSup Example_6_2_8 = 1 sorryAll goals completed! 🐙

Приклад 6.2.9

abbrev Example_6_2_9 : Set EReal := { x | ∃ n:ℕ, x = n+1}

declaration uses 'sorry'example : sInf Example_6_2_9 = 1 := by⊢ sInf Example_6_2_9 = 1 sorryAll goals completed! 🐙

declaration uses 'sorry'example : sSup Example_6_2_9 = ⊤ := by⊢ sSup Example_6_2_9 = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example : sInf (∅ : Set EReal) = ⊤ := by⊢ sInf ∅ = ⊤ sorryAll goals completed! 🐙

declaration uses 'sorry'example (E: Set EReal) : sSup E < sInf E ↔ E = ∅ := byE:Set EReal⊢ sSup E < sInf E ↔ E = ∅ sorryAll goals completed! 🐙

Теорема 6.2.11 (a) / Вправа 6.2.2

theorem declaration uses 'sorry'EReal.mem_le_sup (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sSup E := byE:Set ERealx:ERealhx:x ∈ E⊢ x ≤ sSup E sorryAll goals completed! 🐙

Теорема 6.2.11 (a) / Вправа 6.2.2

theorem declaration uses 'sorry'EReal.mem_ge_inf (E: Set EReal) {x:EReal} (hx: x ∈ E) : x ≤ sInf E := byE:Set ERealx:ERealhx:x ∈ E⊢ x ≤ sInf E sorryAll goals completed! 🐙

Теорема 6.2.11 (b) / Вправа 6.2.2

theorem declaration uses 'sorry'EReal.sup_le_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sSup E ≤ M := byE:Set ERealM:ERealhM:M ∈ upperBounds E⊢ sSup E ≤ M sorryAll goals completed! 🐙

Теорема 6.2.11 (c) / Вправа 6.2.2

theorem declaration uses 'sorry'EReal.inf_ge_upper (E: Set EReal) {M:EReal} (hM: M ∈ upperBounds E) : sInf E ≥ M := byE:Set ERealM:ERealhM:M ∈ upperBounds E⊢ sInf E ≥ M sorryAll goals completed! 🐙

isLUB_iff_sSup_eq.{u_1} {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup s = a#check isLUB_iff_sSup_eq

isLUB_iff_sSup_eq.{u_1} {α : Type u_1} [CompleteSemilatticeSup α] {s : Set α} {a : α} : IsLUB s a ↔ sSup s = a

isGLB_iff_sInf_eq.{u_1} {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a ↔ sInf s = a#check isGLB_iff_sInf_eq

isGLB_iff_sInf_eq.{u_1} {α : Type u_1} [CompleteSemilatticeInf α] {s : Set α} {a : α} : IsGLB s a ↔ sInf s = a

Not in textbook: identify the Chapter 5 extended reals with the Mathlib extended reals.

noncomputable abbrev Chapter5.ExtendedReal.toEReal (x:Chapter5.ExtendedReal) : EReal := match x with
  | real r => ((Chapter5.Real.equivR r):EReal)
  | infty => ⊤
  | neg_infty => ⊥

theorem declaration uses 'sorry'Chapter5.ExtendedReal.coe_inj : Function.Injective toEReal := by⊢ Function.Injective toEReal sorryAll goals completed! 🐙

theorem declaration uses 'sorry'Chapter5.ExtendedReal.coe_surj : Function.Surjective toEReal := by⊢ Function.Surjective toEReal sorryAll goals completed! 🐙

noncomputable abbrev declaration uses 'sorry'declaration uses 'sorry'declaration uses 'sorry'Chapter5.ExtendedReal.equivEReal : Chapter5.ExtendedReal ≃ EReal where
  toFun := toEReal
  invFun := sorry
  left_inv x := byx:ExtendedReal⊢ sorry x.toEReal = x
    sorryAll goals completed! 🐙
  right_inv x := byx:EReal⊢ (sorry x).toEReal = x
    sorryAll goals completed! 🐙