English
If g is an inducing map, then a function g satisfies continuousOn on image f s iff f ∘ g is continuous on s.
Русский
Если g индуциирующее отображение, тогда для всякой s непрерывность на образе f s эквивалентна непрерывности f ∘ g на s.
LaTeX
$$$\\text{IsInducing } f \\Rightarrow (\\text{ContinuousOn } g (f''s) \\iff \\text{ContinuousOn } (g \\circ f) s)$$$
Lean4
theorem continuousOn_image_iff {g : β → γ} {s : Set α} (hf : IsInducing f) :
ContinuousOn g (f '' s) ↔ ContinuousOn (g ∘ f) s := by
simp [ContinuousOn, ContinuousWithinAt, ← hf.map_nhdsWithin_eq]