case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
⊢ ∃ g, EqOn f (↑g) s
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
⊢ ∃ g, EqOn f (↑g) s
obtain ⟨u, hu, uf⟩ :
  ∃ u : E → F, LipschitzWith (lipschitzExtensionConstant F * c) u ∧ EqOn (f - ⇑f') u s :=
  hf.lipschitzOnWith.extend_finite_dimension
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
⊢ ∃ g, EqOn f (↑g) s
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
⊢ ∃ g, EqOn f (↑g) s
let g : E → F := fun x => f' x + u x
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ ∃ g, EqOn f (↑g) s
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
⊢ ∃ g, EqOn f (↑g) s
have fg : EqOn f g s := fun x hx => by simp_rw [← uf hx, Pi.sub_apply, add_sub_cancel'_right]
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)
⊢ ∃ g, EqOn f (↑g) s
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ ∃ g, EqOn f (↑g) s
have hg : ApproximatesLinearOn g (f' : E →L[ℝ] F) univ (lipschitzExtensionConstant F * c) := by
  apply LipschitzOnWith.approximatesLinearOn
  rw [lipschitz_on_univ]
  convert hu
  ext x
  simp only [add_sub_cancel', ContinuousLinearEquiv.coe_coe, Pi.sub_apply]
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)
this : FiniteDimensional ℝ E
⊢ ∃ g, EqOn f (↑g) s
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)
⊢ ∃ g, EqOn f (↑g) s
haveI : FiniteDimensional ℝ E := f'.symm.finiteDimensional
no goals
case intro.intro
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
hg : ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)
this : FiniteDimensional ℝ E
⊢ ∃ g, EqOn f (↑g) s
exact ⟨hg.toHomeomorph g hc, fg⟩
no goals
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
x : E
hx : x ∈ s
⊢ f x = g x
simp_rw [← uf hx, Pi.sub_apply, add_sub_cancel'_right]
case a
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ LipschitzOnWith (lipschitzExtensionConstant F * c) (g - ↑↑f') univ
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ ApproximatesLinearOn g (↑f') univ (lipschitzExtensionConstant F * c)
apply LipschitzOnWith.approximatesLinearOn
case a
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ LipschitzWith (lipschitzExtensionConstant F * c) (g - ↑↑f')
case a
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ LipschitzOnWith (lipschitzExtensionConstant F * c) (g - ↑↑f') univ
rw [lipschitz_on_univ]
case h.e'_6
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ g - ↑↑f' = u
case a
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ LipschitzWith (lipschitzExtensionConstant F * c) (g - ↑↑f')
convert hu
case h.e'_6.h
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
x : E
⊢ (g - ↑↑f') x = u x
case h.e'_6
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
⊢ g - ↑↑f' = u
ext x
no goals
case h.e'_6.h
𝕜 : Type ?u.461349
inst✝¹⁴ : NontriviallyNormedField 𝕜
E✝ : Type ?u.461355
inst✝¹³ : NormedAddCommGroup E✝
inst✝¹² : NormedSpace 𝕜 E✝
F✝ : Type ?u.461465
inst✝¹¹ : NormedAddCommGroup F✝
inst✝¹⁰ : NormedSpace 𝕜 F✝
G : Type ?u.461568
inst✝⁹ : NormedAddCommGroup G
inst✝⁸ : NormedSpace 𝕜 G
G' : Type ?u.461671
inst✝⁷ : NormedAddCommGroup G'
inst✝⁶ : NormedSpace 𝕜 G'
ε : ℝ
inst✝⁵ : CompleteSpace E✝
f✝ : E✝ → F✝
f'✝ : E✝ ≃L[𝕜] F✝
s✝ : Set E✝
c✝ : ℝ≥0
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
F : Type u_2
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : FiniteDimensional ℝ F
s : Set E
f : E → F
f' : E ≃L[ℝ] F
c : ℝ≥0
hf : ApproximatesLinearOn f (↑f') s c
hc : Subsingleton E ∨ lipschitzExtensionConstant F * c < ‖↑(ContinuousLinearEquiv.symm f')‖₊⁻¹
u : E → F
hu : LipschitzWith (lipschitzExtensionConstant F * c) u
uf : EqOn (f - ↑f') u s
g : E → F := fun x => ↑f' x + u x
fg : EqOn f g s
x : E
⊢ (g - ↑↑f') x = u x
simp only [add_sub_cancel', ContinuousLinearEquiv.coe_coe, Pi.sub_apply]