theorem
HasDerivWithinAt.of_inverse
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ f'x₀ g'y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : HasDerivWithinAt g g'y₀ Y y₀)
:
Lemma 10.4.1
theorem
HasDerivWithinAt.of_inverse'
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ f'x₀ g'y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : HasDerivWithinAt g g'y₀ Y y₀)
:
theorem
HasDerivWithinAt.of_inverse_of_zero_deriv
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgf : ∀ x ∈ X, g (f x) = x)
{x₀ y₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f 0 X x₀)
:
¬DifferentiableWithinAt ℝ g Y y₀
theorem
Chapter10.inverse_function_theorem
{X Y : Set ℝ}
{f g : ℝ → ℝ}
(hfXY : ∀ x ∈ X, f x ∈ Y)
(hgYX : ∀ y ∈ Y, g y ∈ X)
(hgf : ∀ x ∈ X, g (f x) = x)
(hfg : ∀ y ∈ Y, f (g y) = y)
{x₀ y₀ f'x₀ : ℝ}
(hx₀ : x₀ ∈ X)
(hfx₀ : f x₀ = y₀)
(hne : f'x₀ ≠ 0)
(hcluster : ClusterPt x₀ (Filter.principal (X \ {x₀})))
(hf : HasDerivWithinAt f f'x₀ X x₀)
(hg : ContinuousWithinAt g Y y₀)
:
HasDerivWithinAt g (1 / f'x₀) Y y₀
Theorem 10.4.2 (Inverse function theorem)