English
As with the previous result but for continuous on a set: g is continuous on s iff its expression in extended charts is continuous on f.extend I '' s.
Русский
Аналогично для непрерывности на множества: g ∣ s непрерывна тогда и только тогда, когда выражение в расширенных картах непрерывно на f.extend I '' s.
LaTeX
$$$\\text{ContinuousOn}_{M\\to M'}(g, s) \\iff \\text{ContinuousOn}_{M\\to M'}(f'.extend I' \\circ g \\circ (f.extend I)^{-1}, f.extend I '' s)$$$
Lean4
/-- If `s ⊆ f.source` and `g x ∈ f'.source` whenever `x ∈ s`, then `g` is continuous on `s` if and
only if `g` written in charts `f.extend I` and `f'.extend I'` is continuous on `f.extend I '' s`. -/
theorem continuousOn_writtenInExtend_iff {f' : OpenPartialHomeomorph M' H'} {g : M → M'} (hs : s ⊆ f.source)
(hmaps : MapsTo g s f'.source) :
ContinuousOn (f'.extend I' ∘ g ∘ (f.extend I).symm) (f.extend I '' s) ↔ ContinuousOn g s :=
by
refine forall_mem_image.trans <| forall₂_congr fun x hx ↦ ?_
refine (continuousWithinAt_congr_set ?_).trans (continuousWithinAt_writtenInExtend_iff _ (hs hx) (hmaps hx) hmaps)
rw [← nhdsWithin_eq_iff_eventuallyEq, ← map_extend_nhdsWithin_eq_image_of_subset, ← map_extend_nhdsWithin]
exacts [hs hx, hs hx, hs]
