α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (restrict s f) x
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ ContinuousOn f s ↔ Continuous (restrict s f)
rw [ContinuousOn, continuous_iff_continuousAt]
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (restrict s f) x

case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (restrict s f) x) → ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) ↔ ∀ (x : ↑s), ContinuousAt (restrict s f) x
constructor
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (restrict s f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : ↑s), ContinuousAt (restrict s f) x) → ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
intro h x xs
no goals
case mpr
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : ↑s), ContinuousAt (restrict s f) x
x : α
xs : x ∈ s
⊢ ContinuousWithinAt f s x
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mpr (h ⟨x, xs⟩)
case mp.mk
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (restrict s f) { val := x, property := xs }
case mp
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
⊢ (∀ (x : α), x ∈ s → ContinuousWithinAt f s x) → ∀ (x : ↑s), ContinuousAt (restrict s f) x
rintro h ⟨x, xs⟩
no goals
case mp.mk
α : Type u_1
β : Type u_2
γ : Type ?u.312868
δ : Type ?u.312871
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
s : Set α
h : ∀ (x : α), x ∈ s → ContinuousWithinAt f s x
x : α
xs : x ∈ s
⊢ ContinuousAt (restrict s f) { val := x, property := xs }
exact (continuousWithinAt_iff_continuousAt_restrict f xs).mp (h x xs)