𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.328214
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.328309
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
h : ∀ (x : E), x ∈ s → ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s x
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.328214
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.328309
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x : E
s t : Set E
L L₁ L₂ : Filter E
h : ∀ (x : E), x ∈ s → ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
⊢ DifferentiableOn 𝕜 f s
intro x xs
case intro.intro.intro
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.328214
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.328309
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t✝ : Set E
L L₁ L₂ : Filter E
h : ∀ (x : E), x ∈ s → ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 f s x
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.328214
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.328309
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t : Set E
L L₁ L₂ : Filter E
h : ∀ (x : E), x ∈ s → ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
⊢ DifferentiableWithinAt 𝕜 f s x
rcases h x xs with ⟨t, t_open, xt, ht⟩
no goals
case intro.intro.intro
𝕜 : Type u_2
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type u_1
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type u_3
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
G : Type ?u.328214
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
G' : Type ?u.328309
inst✝¹ : NormedAddCommGroup G'
inst✝ : NormedSpace 𝕜 G'
f f₀ f₁ g : E → F
f' f₀' f₁' g' e : E →L[𝕜] F
x✝ : E
s t✝ : Set E
L L₁ L₂ : Filter E
h : ∀ (x : E), x ∈ s → ∃ u, IsOpen u ∧ x ∈ u ∧ DifferentiableOn 𝕜 f (s ∩ u)
x : E
xs : x ∈ s
t : Set E
t_open : IsOpen t
xt : x ∈ t
ht : DifferentiableOn 𝕜 f (s ∩ t)
⊢ DifferentiableWithinAt 𝕜 f s x
exact (differentiableWithinAt_inter (IsOpen.mem_nhds t_open xt)).1 (ht x ⟨xs, xt⟩)