no goals
α : Type u
β : Type v
γ : Type ?u.160981
δ : Type ?u.160984
ε : Type ?u.160987
ζ : Type ?u.160990
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
p : α → Prop
f : α → β
t : Set β
h1 : ∀ (x : α), f x ∈ t
x : α
⊢ ContinuousAt (codRestrict f t h1) x ↔ ContinuousAt f x
simp_rw [inducing_subtype_val.continuousAt_iff, Function.comp, val_codRestrict_apply]