𝕜 : 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
⊢ ContinuousOn f 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
⊢ ContinuousOn f s ↔ ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
refine' ⟨fun h y => (ContinuousLinearMap.apply 𝕜 F y).continuous.comp_continuousOn h, fun h => _⟩
𝕜 : 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
⊢ ContinuousOn f 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
⊢ ContinuousOn f s
let d := finrank 𝕜 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
⊢ ContinuousOn f 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
⊢ ContinuousOn f s
have hd : d = finrank 𝕜 (Fin d → 𝕜) := (finrank_fin_fun 𝕜).symm
𝕜 : 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
⊢ ContinuousOn f 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
⊢ ContinuousOn f s
let e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
𝕜 : 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.arrowCongr e₁ 1) (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContinuousOn f 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
⊢ ContinuousOn f s
let e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  (e₁.arrowCongr (1 : F ≃L[𝕜] F)).trans (ContinuousLinearEquiv.piRing (Fin d))
𝕜 : 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.arrowCongr e₁ 1) (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContinuousOn ((↑(ContinuousLinearEquiv.symm e₂) ∘ ↑e₂) ∘ f) 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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.arrowCongr e₁ 1) (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContinuousOn f s
rw [← Function.comp.left_id f, ← e₂.symm_comp_self]
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 𝕜
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : FiniteDimensional 𝕜 E
f : X → E →L[𝕜] F
s : Set X
h : ∀ (y : E), ContinuousOn (fun x => ↑(f x) y) s
d : ℕ := finrank 𝕜 E
hd : d = finrank 𝕜 (Fin d → 𝕜)
e₁ : E ≃L[𝕜] Fin d → 𝕜 := ContinuousLinearEquiv.ofFinrankEq hd
e₂ : (E →L[𝕜] F) ≃L[𝕜] Fin d → F :=
  ContinuousLinearEquiv.trans (ContinuousLinearEquiv.arrowCongr e₁ 1) (ContinuousLinearEquiv.piRing (Fin d))
⊢ ContinuousOn ((↑(ContinuousLinearEquiv.symm e₂) ∘ ↑e₂) ∘ f) s
exact e₂.symm.continuous.comp_continuousOn (continuousOn_pi.mpr fun i => h _)