α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
⊢ ContinuousOn f s
intro x xs
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
rcases h x xs with ⟨t, open_t, xt, ct⟩
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
⊢ ContinuousWithinAt f s x
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
⊢ ContinuousWithinAt f s x
have := ct x ⟨xs, xt⟩
no goals
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type ?u.347413
δ : Type ?u.347416
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ∃ t, IsOpen t ∧ x ∈ t ∧ ContinuousOn f (s ∩ t)
x : α
xs : x ∈ s
t : Set α
open_t : IsOpen t
xt : x ∈ t
ct : ContinuousOn f (s ∩ t)
this : ContinuousWithinAt f (s ∩ t) x
⊢ ContinuousWithinAt f s x
rwa [ContinuousWithinAt, ← nhdsWithin_restrict _ xt open_t] at this