English
Continuity of a composition with an open partial homeomorphism holds under a subset assumption: if s ⊆ e.target, then ContinuousOn f s iff ContinuousOn (f ∘ e) (e.source ∩ e^{-1} s).
Русский
Непрерывность композиции с открытым частичным гомеоморфизмом сохраняется при подмножестве: s ⊆ e.target тогда ContinuousOn f s ⇔ ContinuousOn (f ∘ e) (e.source ∩ e^{-1} s).
LaTeX
$$$\forall f s,\ s ⊆ e.target \Rightarrow ContinuousOn f s \Leftrightarrow ContinuousOn (f \circ e) (e.source \cap e^{-1} s)$$$
Lean4
/-- A function is continuous on a set if and only if its composition with an open partial
homeomorphism on the right is continuous on the corresponding set. -/
theorem continuousOn_iff_continuousOn_comp_right {f : Y → Z} {s : Set Y} (h : s ⊆ e.target) :
ContinuousOn f s ↔ ContinuousOn (f ∘ e) (e.source ∩ e ⁻¹' s) :=
by
simp only [← e.symm_image_eq_source_inter_preimage h, ContinuousOn, forall_mem_image]
refine forall₂_congr fun x hx => ?_
rw [e.continuousWithinAt_iff_continuousWithinAt_comp_right (h hx), e.symm_image_eq_source_inter_preimage h,
inter_comm, continuousWithinAt_inter]
exact IsOpen.mem_nhds e.open_source (e.map_target (h hx))
