English
If a function g from M to M' has its source image in f'.source and can be written in charts f.extend I and f'.extend I', then g is continuous on s iff the rewritten form in charts is continuous on f.extend I '' s.
Русский
Если функция g: M → M' имеет образ в f'.source и может быть записана в схематических картах f.extend I и f'.extend I', то непрерывность на s эквивалентна непрерывности в записей по этим картам.
LaTeX
$$$\\text{ContinuousWithinAt or ContinuousOn equivalences: }\\;\\text{nhdsWithin}\\;_1 \\iff \\text{nhdsWithin}\\;_2$$$
Lean4
theorem continuousWithinAt_writtenInExtend_iff {f' : OpenPartialHomeomorph M' H'} {g : M → M'} {y : M}
(hy : y ∈ f.source) (hgy : g y ∈ f'.source) (hmaps : MapsTo g s f'.source) :
ContinuousWithinAt (f'.extend I' ∘ g ∘ (f.extend I).symm) ((f.extend I).symm ⁻¹' s ∩ range I) (f.extend I y) ↔
ContinuousWithinAt g s y :=
by
unfold ContinuousWithinAt
simp only [comp_apply]
rw [extend_left_inv _ hy, f'.tendsto_extend_comp_iff _ hgy, ← f.map_extend_symm_nhdsWithin (I := I) hy,
tendsto_map'_iff]
rw [← f.map_extend_nhdsWithin (I := I) hy, eventually_map]
filter_upwards [inter_mem_nhdsWithin _ (f.open_source.mem_nhds hy)] with z hz
rw [comp_apply, extend_left_inv _ hz.2]
exact
hmaps
hz.1
-- there is no definition `writtenInExtend` but we already use some made-up names in this file
