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

          Аналіз I, Глава 9.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:

              Recalling basic pointwise operations on functions
namespace Chapter9open Classical in
noncomputable abbrev function_example : ℝ → ℝ := fun x ↦ if x ∈ ((fun y:ℚ ↦ (y:ℝ)) '' Set.univ) then 1 else 0
            Визначення 9.2.1 (Arithmetic operations on functions)
theorem add_func_eval (f g: ℝ → ℝ) (x: ℝ) : (f + g) x = f x + g x := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ (f + g) x = f x + g x
  rflAll goals completed! 🐙
theorem sub_func_eval (f g: ℝ → ℝ) (x: ℝ) : (f - g) x = f x - g x := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ (f - g) x = f x - g x
  rflAll goals completed! 🐙theorem max_func_eval (f g: ℝ → ℝ) (x: ℝ) : max f g x = max (f x) (g x) := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ max f g x = max (f x) (g x)
  rflAll goals completed! 🐙theorem min_func_eval (f g: ℝ → ℝ) (x: ℝ) : min f g x = min (f x) (g x) := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ min f g x = min (f x) (g x)
  rflAll goals completed! 🐙theorem mul_func_eval (f g: ℝ → ℝ) (x: ℝ) : (f * g) x = f x * g x := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ (f * g) x = f x * g x
  rflAll goals completed! 🐙theorem div_func_eval (f g: ℝ → ℝ) (x: ℝ) : (f / g) x = f x / g x := byf:ℝ → ℝg:ℝ → ℝx:ℝ⊢ (f / g) x = f x / g x
  rflAll goals completed! 🐙theorem smul_func_eval (c: ℝ) (f: ℝ → ℝ) (x: ℝ) : (c • f) x = c * f x := byc:ℝf:ℝ → ℝx:ℝ⊢ (c • f) x = c * f x
  rflAll goals completed! 🐙abbrev f_9_2_2 : ℝ → ℝ := fun x ↦ x^2abbrev g_9_2_2 : ℝ → ℝ := fun x ↦ 2*xexample : f_9_2_2 + g_9_2_2 = fun x ↦ x^2 + 2*x := by⊢ f_9_2_2 + g_9_2_2 = fun x => x ^ 2 + 2 * x
  rflAll goals completed! 🐙example : f_9_2_2 * g_9_2_2 = fun x ↦ 2 * x^3 := by⊢ f_9_2_2 * g_9_2_2 = fun x => 2 * x ^ 3 ext xhx:ℝ⊢ (f_9_2_2 * g_9_2_2) x = 2 * x ^ 3; simphx:ℝ⊢ f_9_2_2 x * g_9_2_2 x = 2 * x ^ 3; ringAll goals completed! 🐙example : f_9_2_2 - g_9_2_2 = fun x ↦ x^2 - 2*x := by⊢ f_9_2_2 - g_9_2_2 = fun x => x ^ 2 - 2 * x
  rflAll goals completed! 🐙example : 6 • f_9_2_2 = fun x ↦ 6 * (x^2) := by⊢ 6 • f_9_2_2 = fun x => 6 * x ^ 2 ext xhx:ℝ⊢ (6 • f_9_2_2) x = 6 * x ^ 2; simpAll goals completed! 🐙example : f_9_2_2 ∘ g_9_2_2 = fun x ↦ 4*x^2 := by⊢ f_9_2_2 ∘ g_9_2_2 = fun x => 4 * x ^ 2 ext xhx:ℝ⊢ (f_9_2_2 ∘ g_9_2_2) x = 4 * x ^ 2; simphx:ℝ⊢ f_9_2_2 (g_9_2_2 x) = 4 * x ^ 2; ringAll goals completed! 🐙example : g_9_2_2 ∘ f_9_2_2 = fun x ↦ 2*x^2 := by⊢ g_9_2_2 ∘ f_9_2_2 = fun x => 2 * x ^ 2 ext xhx:ℝ⊢ (g_9_2_2 ∘ f_9_2_2) x = 2 * x ^ 2; simpAll goals completed! 🐙/- Exercise 9.2.1.  -/

def declaration uses 'sorry'Exercise_9_2_1a : Decidable (∀ (f g h : ℝ → ℝ), (f+g) ∘ h = f ∘ h + g ∘ h) := by⊢ Decidable (∀ (f g h : ℝ → ℝ), (f + g) ∘ h = f ∘ h + g ∘ h)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_9_2_1b : Decidable (∀ (f g h : ℝ → ℝ), f ∘ (g + h) = f ∘ g + f ∘ h) := by⊢ Decidable (∀ (f g h : ℝ → ℝ), f ∘ (g + h) = f ∘ g + f ∘ h)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_9_2_1c : Decidable (∀ (f g h : ℝ → ℝ), (f+g) * h = f * h + g * h) := by⊢ Decidable (∀ (f g h : ℝ → ℝ), (f + g) * h = f * h + g * h)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙def declaration uses 'sorry'Exercise_9_2_1d : Decidable (∀ (f g h : ℝ → ℝ), f * (g+h) = f * g + f * h) := by⊢ Decidable (∀ (f g h : ℝ → ℝ), f * (g + h) = f * g + f * h)
  -- The first line of this construction should be `apply isTrue` or `apply isFalse`.
  sorryAll goals completed! 🐙end Chapter9