A `ContinuousOn` version of `Continuous.subtype_mk`

Stream: Is there code for X?

[Michael Lee]

I'm looking for a result that's something like

theorem ContinuousOn.subtype_mk (h : ContinuousOn f s) (hp : ∀ x, p (f x)) : ContinuousOn (fun x => (⟨f x, hp x⟩ : Subtype p)) s

Is there anything like this already?

[Michael Lee]

Or possibly something like this?

theorem ContinuousOn.subtype_mk (h : ContinuousOn f s) (hp : ∀ x ∈ s, p (f x)) :
  ContinuousOn (fun x (hx : x ∈ s) => (⟨f x, hp x hx⟩ : Subtype p)) s

[Jireh Loreaux]

I don't think we have it, but you should be able to prove it using docs#ContinuousOn.restrict and docs#continuous_induced_rng