α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : ¬x ∈ closure s
⊢ ContinuousWithinAt f s x
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
⊢ ¬x ∈ closure s → ContinuousWithinAt f s x
intro hx
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : ¬x ∈ closure s
⊢ ContinuousWithinAt f s x
rw [mem_closure_iff_nhdsWithin_neBot, neBot_iff, not_not] at hx
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ ContinuousWithinAt f s x
rw [ContinuousWithinAt, hx]
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.370490
δ : Type ?u.370493
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
x : α
hx : 𝓝[s] x = ⊥
⊢ Tendsto f ⊥ (𝓝 (f x))
exact tendsto_bot