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

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:

Review of Mathlib monotonicity concepts

namespace Chapter9

Визначення 9.8.1

theorem MonotoneOn.iff {X: Set ℝ} (f: ℝ → ℝ) : MonotoneOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x := byX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x) → MonotoneOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ MonotoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f x intro h x hx y hy hxympX:Set ℝf:ℝ → ℝh:MonotoneOn f Xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:y > x⊢ f y ≥ f x
    exact h hx hy (le_of_lt hxy)All goals completed! 🐙
  intro h x hx y hy hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x ≤ y⊢ f x ≤ f y
  rw [le_iff_lt_or_eq] at hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y ∨ x = y⊢ f x ≤ f y
  rcases hxy with hxy | hxympr.inlX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f x ≤ f ympr.inrX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x = y⊢ f x ≤ f y
  .mpr.inlX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≥ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f x ≤ f y exact h x hx y hy hxyAll goals completed! 🐙
  simp [hxy]All goals completed! 🐙

theorem StrictMono.iff {X: Set ℝ} (f: ℝ → ℝ) : StrictMonoOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x := byX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x) → StrictMonoOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ StrictMonoOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y > f x intro h x hx y hy hxympX:Set ℝf:ℝ → ℝh:StrictMonoOn f Xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:y > x⊢ f y > f x
    exact h hx hy hxyAll goals completed! 🐙
  intro h x hx y hy hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y > f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f x < f y
  exact h x hx y hy hxyAll goals completed! 🐙

theorem AntitoneOn.iff {X: Set ℝ} (f: ℝ → ℝ) : AntitoneOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x := byX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x) → AntitoneOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ AntitoneOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f x intro h x hx y hy hxympX:Set ℝf:ℝ → ℝh:AntitoneOn f Xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:y > x⊢ f y ≤ f x
    exact h hx hy (le_of_lt hxy)All goals completed! 🐙
  intro h x hx y hy hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x ≤ y⊢ f y ≤ f x
  rw [le_iff_lt_or_eq] at hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y ∨ x = y⊢ f y ≤ f x
  rcases hxy with hxy | hxympr.inlX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f y ≤ f xmpr.inrX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x = y⊢ f y ≤ f x
  .mpr.inlX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y ≤ f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f y ≤ f x exact h x hx y hy hxyAll goals completed! 🐙
  simp [hxy]All goals completed! 🐙

theorem StrictAntitone.iff {X: Set ℝ} (f: ℝ → ℝ) : StrictAntiOn f X  ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x := byX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X ↔ ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x
  constructormpX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f xmprX:Set ℝf:ℝ → ℝ⊢ (∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x) → StrictAntiOn f X
  .mpX:Set ℝf:ℝ → ℝ⊢ StrictAntiOn f X → ∀ x ∈ X, ∀ y ∈ X, y > x → f y < f x intro h x hx y hy hxympX:Set ℝf:ℝ → ℝh:StrictAntiOn f Xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:y > x⊢ f y < f x
    exact h hx hy hxyAll goals completed! 🐙
  intro h x hx y hy hxymprX:Set ℝf:ℝ → ℝh:∀ x ∈ X, ∀ y ∈ X, y > x → f y < f xx:ℝhx:x ∈ Xy:ℝhy:y ∈ Xhxy:x < y⊢ f y < f x
  exact h x hx y hy hxyAll goals completed! 🐙

Приклади 9.8.2

declaration uses 'sorry'example : StrictMonoOn (fun x:ℝ ↦ x^2) (Set.Ici 0) := by⊢ StrictMonoOn (fun x => x ^ 2) (Set.Ici 0) sorryAll goals completed! 🐙

declaration uses 'sorry'example : StrictAntiOn (fun x:ℝ ↦ x^2) (Set.Iic 0) := by⊢ StrictAntiOn (fun x => x ^ 2) (Set.Iic 0) sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ MonotoneOn (fun x:ℝ ↦ x^2) Set.univ := by⊢ ¬MonotoneOn (fun x => x ^ 2) Set.univ sorryAll goals completed! 🐙

declaration uses 'sorry'example : ¬ AntitoneOn (fun x:ℝ ↦ x^2) Set.univ := by⊢ ¬AntitoneOn (fun x => x ^ 2) Set.univ sorryAll goals completed! 🐙

declaration uses 'sorry'example {X:Set ℝ} {f:ℝ → ℝ} (hf: StrictMonoOn f X) : MonotoneOn f X := byX:Set ℝf:ℝ → ℝhf:StrictMonoOn f X⊢ MonotoneOn f X sorryAll goals completed! 🐙

declaration uses 'sorry'example (X:Set ℝ) : MonotoneOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝ⊢ MonotoneOn (fun x => 6) X sorryAll goals completed! 🐙

declaration uses 'sorry'example (X:Set ℝ) : AntitoneOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝ⊢ AntitoneOn (fun x => 6) X sorryAll goals completed! 🐙

nontrivial_iff.{u_1} {α : Type u_1} : Nontrivial α ↔ ∃ x y, x ≠ y#check nontrivial_iff

nontrivial_iff.{u_1} {α : Type u_1} : Nontrivial α ↔ ∃ x y, x ≠ y

declaration uses 'sorry'example {X:Set ℝ} (hX: Nontrivial X) : ¬ StrictMonoOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝhX:Nontrivial ↑X⊢ ¬StrictMonoOn (fun x => 6) X sorryAll goals completed! 🐙

declaration uses 'sorry'example (X:Set ℝ) (hX: Nontrivial X) : ¬ StrictAntiOn (fun x:ℝ ↦ (6:ℝ)) X := byX:Set ℝhX:Nontrivial ↑X⊢ ¬StrictAntiOn (fun x => 6) X sorryAll goals completed! 🐙

declaration uses 'sorry'example : ∃ (X:Set ℝ) (f:ℝ → ℝ), ContinuousOn f X ∧ ¬ MonotoneOn f X ∧ ¬ AntitoneOn f X := by⊢ ∃ X f, ContinuousOn f X ∧ ¬MonotoneOn f X ∧ ¬AntitoneOn f X sorryAll goals completed! 🐙

declaration uses 'sorry'example : ∃ (X:Set ℝ) (f:ℝ → ℝ), MonotoneOn f X ∧ ¬ ContinuousOn f X := by⊢ ∃ X f, MonotoneOn f X ∧ ¬ContinuousOn f X sorryAll goals completed! 🐙

Твердження 9.8.3 / Вправа 9.8.4

theorem declaration uses 'sorry'MonotoneOn.exist_inverse {a b:ℝ} (h: a < b) (f: ℝ → ℝ) (hcont: ContinuousOn f (Set.Icc a b)) (hmono: StrictMonoOn f (Set.Icc a b)) :
  f '' (Set.Icc a b) = Set.Icc (f a) (f b) ∧
  ∃ finv: ℝ → ℝ, ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
  finv '' (Set.Icc (f a) (f b)) = Set.Icc a b ∧
  (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
  ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y
   := bya:ℝb:ℝh:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)hmono:StrictMonoOn f (Set.Icc a b)⊢ f '' Set.Icc a b = Set.Icc (f a) (f b) ∧
  ∃ finv,
    ContinuousOn finv (Set.Icc (f a) (f b)) ∧
      StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
        finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧
          (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y
  sorryAll goals completed! 🐙

Приклад 9.8.4

example {R :ℝ} (hR: R > 0) {n:ℕ} (hn: n > 0) : ∃ g : ℝ → ℝ, ∀ x ∈ Set.Icc 0 (R^n), (g x)^n = x := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
  set f : ℝ → ℝ := fun x ↦ x^nR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ n⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
  have hcont : ContinuousOn f (Set.Icc 0 R) := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x fun_propAll goals completed! 🐙
  have hmono : StrictMonoOn f (Set.Icc 0 R) := byR:ℝhR:R > 0n:ℕhn:n > 0⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
    intro x hx y hy hxyR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝhx:x ∈ Set.Icc 0 Ry:ℝhy:y ∈ Set.Icc 0 Rhxy:x < y⊢ f x < f y
    simp at hxR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝy:ℝhy:y ∈ Set.Icc 0 Rhxy:x < yhx:0 ≤ x ∧ x ≤ R⊢ f x < f y
    simp [f]R:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝy:ℝhy:y ∈ Set.Icc 0 Rhxy:x < yhx:0 ≤ x ∧ x ≤ R⊢ x ^ n < y ^ n
    exact pow_lt_pow_left₀ hxy (byR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝy:ℝhy:y ∈ Set.Icc 0 Rhxy:x < yhx:0 ≤ x ∧ x ≤ R⊢ 0 ≤ x contrapose! hnR:ℝhR:R > 0n:ℕf:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝy:ℝhy:y ∈ Set.Icc 0 Rhxy:x < yhx:0 ≤ x ∧ x ≤ Rhn:x < 0⊢ n ≤ 0; linarithAll goals completed! 🐙) (byR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)x:ℝy:ℝhy:y ∈ Set.Icc 0 Rhxy:x < yhx:0 ≤ x ∧ x ≤ R⊢ n ≠ 0 linarithAll goals completed! 🐙)
  obtain ⟨ g, ⟨ _, _, _, _, hg⟩ ⟩ := (MonotoneOn.exist_inverse (byR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)hmono:StrictMonoOn f (Set.Icc 0 R)⊢ 0 < R positivityAll goals completed! 🐙) f hcont hmono).2
  simp only [and_imp, f, zero_pow (by positivity)] at hgintro.intro.intro.intro.introR:ℝhR:R > 0n:ℕhn:n > 0f:ℝ → ℝ := fun x => x ^ nhcont:ContinuousOn f (Set.Icc 0 R)hmono:StrictMonoOn f (Set.Icc 0 R)g:ℝ → ℝleft✝³:ContinuousOn g (Set.Icc (f 0) (f R))left✝²:StrictMonoOn g (Set.Icc (f 0) (f R))left✝¹:g '' Set.Icc (f 0) (f R) = Set.Icc 0 Rleft✝:∀ x ∈ Set.Icc 0 R, g (f x) = xhg:∀ y ∈ Set.Icc 0 (R ^ n), g y ^ n = y⊢ ∃ g, ∀ x ∈ Set.Icc 0 (R ^ n), g x ^ n = x
  use gAll goals completed! 🐙

Вправа 9.8.1

theorem declaration uses 'sorry'IsMaxOn.of_monotone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: MonotoneOn f (Set.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:MonotoneOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙

theorem declaration uses 'sorry'IsMaxOn.of_strictmono_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: StrictMonoOn f (Set.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:StrictMonoOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙

theorem declaration uses 'sorry'IsMaxOn.of_antitone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: AntitoneOn f (Set.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:AntitoneOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax sorryAll goals completed! 🐙

theorem declaration uses 'sorry'IsMaxOn.of_strictantitone_on_compact {a b:ℝ} (h:a < b) {f:ℝ → ℝ} (hf: StrictAntiOn f (Set.Icc a b)) :
  ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:StrictAntiOn f (Set.Icc a b)⊢ ∃ xmax ∈ Set.Icc a b, IsMaxOn f (Set.Icc a b) xmax
  sorryAll goals completed! 🐙

Вправа 9.8.2

theorem declaration uses 'sorry'no_strictmono_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictMonoOn f (Set.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : StrictMonoOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'no_monotone_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: MonotoneOn f (Set.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : MonotoneOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'no_strictanti_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: StrictAntiOn f (Set.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : StrictAntiOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) sorryAll goals completed! 🐙

theorem declaration uses 'sorry'no_antitone_intermediate_value : ∃ (a b:ℝ) (hab: a < b) (f:ℝ → ℝ) (hf: AntitoneOn f (Set.Icc a b)), ¬ ∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) := by⊢ ∃ a b, ∃ (_ : a < b), ∃ f, ∃ (_ : AntitoneOn f (Set.Icc a b)), ¬∃ y, y ∈ Set.Icc (f a) (f b) ∨ y ∈ Set.Icc (f a) (f b) sorryAll goals completed! 🐙

Вправа 9.8.3

theorem declaration uses 'sorry'mono_of_continuous_inj {a b:ℝ} (h: a < b) {f:ℝ → ℝ}
  (hf: ContinuousOn f (Set.Icc a b))
  (hinj: Function.Injective (fun x: Set.Icc a b ↦ f x )) :
  StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b) := bya:ℝb:ℝh:a < bf:ℝ → ℝhf:ContinuousOn f (Set.Icc a b)hinj:Function.Injective fun x => f ↑x⊢ StrictMonoOn f (Set.Icc a b) ∨ StrictAntiOn f (Set.Icc a b)
  sorryAll goals completed! 🐙

Вправа 9.8.4

def declaration uses 'sorry'MonotoneOn.exist_inverse_without_continuity {a b:ℝ} (h: a < b) (f: ℝ → ℝ) (hmono: StrictMonoOn f (Set.Icc a b)) :
  Decidable ( f '' (Set.Icc a b) = Set.Icc (f a) (f b) ∧
  ∃ finv: ℝ → ℝ, ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
  finv '' (Set.Icc (f a) (f b)) = Set.Icc a b ∧
  (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
  ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y )
   := bya:ℝb:ℝh:a < bf:ℝ → ℝhmono:StrictMonoOn f (Set.Icc a b)⊢ Decidable
  (f '' Set.Icc a b = Set.Icc (f a) (f b) ∧
    ∃ finv,
      ContinuousOn finv (Set.Icc (f a) (f b)) ∧
        StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
          finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧
            (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y)
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

Вправа 9.8.4

def declaration uses 'sorry'MonotoneOn.exist_inverse_without_strictmono {a b:ℝ} (h: a < b) (f: ℝ → ℝ)
  (hcont: ContinuousOn f (Set.Icc a b)) (hmono: MonotoneOn f (Set.Icc a b)) :
  Decidable ( f '' (Set.Icc a b) = Set.Icc (f a) (f b) ∧
  ∃ finv: ℝ → ℝ, ContinuousOn finv (Set.Icc (f a) (f b)) ∧ StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
  finv '' (Set.Icc (f a) (f b)) = Set.Icc a b ∧
  (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧
  ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y )
   := bya:ℝb:ℝh:a < bf:ℝ → ℝhcont:ContinuousOn f (Set.Icc a b)hmono:MonotoneOn f (Set.Icc a b)⊢ Decidable
  (f '' Set.Icc a b = Set.Icc (f a) (f b) ∧
    ∃ finv,
      ContinuousOn finv (Set.Icc (f a) (f b)) ∧
        StrictMonoOn finv (Set.Icc (f a) (f b)) ∧
          finv '' Set.Icc (f a) (f b) = Set.Icc a b ∧
            (∀ x ∈ Set.Icc a b, finv (f x) = x) ∧ ∀ y ∈ Set.Icc (f a) (f b), f (finv y) = y)
  -- перший рядок цієї конструкції має бути або `apply isTrue`, або `apply isFalse`.
  sorryAll goals completed! 🐙

/- Вправа 9.8.4: state and prove an analogue of `MonotoneOne.exist_inverse` for `Antitone` functions. -/
-- theorem AntitoneOn.exist_inverse {a b:ℝ} (h: a < b) (f: ℝ → ℝ) (hcont: ContinuousOn f (Set.Icc a b)) (hmono: StrictAntiOn f (Set.Icc a b)) : sorry := by sorry

An equivalence between the natural numbers and the rationals.

noncomputable abbrev q_9_8_5 : ℕ ≃ ℚ := nonempty_equiv_of_countable.some

noncomputable abbrev g_9_8_5 : ℚ → ℝ := fun q ↦ (2:ℝ)^(-q_9_8_5.symm q:ℤ)noncomputable abbrev f_9_8_5 : ℝ → ℝ := fun x ↦ ∑' r : {r:ℚ // (r:ℝ) < x}, g_9_8_5 r

Вправа 9.8.5(a)

declaration uses 'sorry'example : StrictMonoOn f_9_8_5 Set.univ := by⊢ StrictMonoOn f_9_8_5 Set.univ
  sorryAll goals completed! 🐙

Вправа 9.8.5(b)

declaration uses 'sorry'example (r:ℚ) : ¬ ContinuousAt f_9_8_5 r := byr:ℚ⊢ ¬ContinuousAt f_9_8_5 ↑r
  sorryAll goals completed! 🐙

Вправа 9.8.5(c)

declaration uses 'sorry'example {x:ℝ} (hx: ¬ ∃ r:ℚ, x = r) : ContinuousAt f_9_8_5 x := byx:ℝhx:¬∃ r, x = ↑r⊢ ContinuousAt f_9_8_5 x
  sorryAll goals completed! 🐙

end Chapter9