𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
let ι : Type _ := Basis.ofVectorSpaceIndex ℝ E'
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
let A := (Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have LA : LipschitzWith ‖A.toContinuousLinearMap‖₊ A := by apply A.lipschitz
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
have L : LipschitzOnWith (‖A.toContinuousLinearMap‖₊ * K) (A ∘ f) s :=
  LA.comp_lipschitzOnWith hf
case intro.intro
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
obtain ⟨g, hg, gs⟩ :
  ∃ g : α → ι → ℝ, LipschitzWith (‖A.toContinuousLinearMap‖₊ * K) g ∧ EqOn (A ∘ f) g s :=
  L.extend_pi
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ LipschitzWith (lipschitzExtensionConstant E' * K) (↑(ContinuousLinearEquiv.symm A) ∘ g)

case intro.intro.refine'_2
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ EqOn f (↑(ContinuousLinearEquiv.symm A) ∘ g) s
case intro.intro
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ ∃ g, LipschitzWith (lipschitzExtensionConstant E' * K) g ∧ EqOn f g s
refine' ⟨A.symm ∘ g, _, _⟩
no goals
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
⊢ LipschitzWith ‖↑A‖₊ ↑A
apply A.lipschitz
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ LipschitzWith (lipschitzExtensionConstant E' * K) (↑(ContinuousLinearEquiv.symm A) ∘ g)
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ LipschitzWith (lipschitzExtensionConstant E' * K) (↑(ContinuousLinearEquiv.symm A) ∘ g)
have LAsymm : LipschitzWith ‖A.symm.toContinuousLinearMap‖₊ A.symm := by
  apply A.symm.lipschitz
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ ‖↑(ContinuousLinearEquiv.symm A)‖₊ * (‖↑A‖₊ * K) ≤ lipschitzExtensionConstant E' * K
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ LipschitzWith (lipschitzExtensionConstant E' * K) (↑(ContinuousLinearEquiv.symm A) ∘ g)
apply (LAsymm.comp hg).weaken
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ ‖↑(ContinuousLinearEquiv.symm A)‖₊ * ‖↑A‖₊ * K ≤
    (let A := LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'));
      max (‖↑(ContinuousLinearEquiv.symm A)‖₊ * ‖↑A‖₊) 1) *
      K
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ ‖↑(ContinuousLinearEquiv.symm A)‖₊ * (‖↑A‖₊ * K) ≤ lipschitzExtensionConstant E' * K
rw [lipschitzExtensionConstant, ← mul_assoc]
no goals
case intro.intro.refine'_1
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
LAsymm : LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
⊢ ‖↑(ContinuousLinearEquiv.symm A)‖₊ * ‖↑A‖₊ * K ≤
    (let A := LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'));
      max (‖↑(ContinuousLinearEquiv.symm A)‖₊ * ‖↑A‖₊) 1) *
      K
refine' mul_le_mul' (le_max_left _ _) le_rfl
no goals
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ LipschitzWith ‖↑(ContinuousLinearEquiv.symm A)‖₊ ↑(ContinuousLinearEquiv.symm A)
apply A.symm.lipschitz
case intro.intro.refine'_2
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
x : α
hx : x ∈ s
⊢ f x = (↑(ContinuousLinearEquiv.symm A) ∘ g) x
case intro.intro.refine'_2
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
⊢ EqOn f (↑(ContinuousLinearEquiv.symm A) ∘ g) s
intro x hx
case intro.intro.refine'_2
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
x : α
hx : x ∈ s
this : ↑A (f x) = g x
⊢ f x = (↑(ContinuousLinearEquiv.symm A) ∘ g) x
case intro.intro.refine'_2
𝕜 : Type u
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace 𝕜 E
F : Type w
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace 𝕜 F
F' : Type x
inst✝⁹ : AddCommGroup F'
inst✝⁸ : Module 𝕜 F'
inst✝⁷ : TopologicalSpace F'
inst✝⁶ : TopologicalAddGroup F'
inst✝⁵ : ContinuousSMul 𝕜 F'
inst✝⁴ : CompleteSpace 𝕜
α : Type u_1
inst✝³ : PseudoMetricSpace α
E' : Type u_2
inst✝² : NormedAddCommGroup E'
inst✝¹ : NormedSpace ℝ E'
inst✝ : FiniteDimensional ℝ E'
s : Set α
f : α → E'
K : ℝ≥0
hf : LipschitzOnWith K f s
ι : Type u_2 := ↑(Basis.ofVectorSpaceIndex ℝ E')
A : E' ≃L[ℝ] ↑(Basis.ofVectorSpaceIndex ℝ E') → ℝ :=
  LinearEquiv.toContinuousLinearEquiv (Basis.equivFun (Basis.ofVectorSpace ℝ E'))
LA : LipschitzWith ‖↑A‖₊ ↑A
L : LipschitzOnWith (‖↑A‖₊ * K) (↑A ∘ f) s
g : α → ι → ℝ
hg : LipschitzWith (‖↑A‖₊ * K) g
gs : EqOn (↑A ∘ f) g s
x : α
hx : x ∈ s
⊢ f x = (↑(ContinuousLinearEquiv.symm A) ∘ g) x
have : A (f x) = g x := gs hx