lean_workbook_plus_49379

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Let $f(x) = \sqrt {6-x}, g(x)= \sqrt {3-x}.$ Then the expression is $\frac{f(x) - f(2)}{g(x)-g(2)} = \frac{(f(x) - f(2))/(x-2)}{(g(x)-g(2))/(x-2)}$ . By the definition of the derivative, find the limit as $x \rightarrow 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49379 (f g : ℝ → ℝ) (x : ℝ) (hf : f = fun (x:ℝ) => (6 - x)^(1 / 2)) (hg : g = fun (x:ℝ) => (3 - x)^(1 / 2)) : (f x - f 2) / (g x - g 2) = (f x - f 2) / (x - 2) * (x - 2) / (g x - g 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph