English
If f is an inducing map, then a function g is continuous on the image f s iff g ∘ f is continuous on s.
Русский
Если f индуцирующее отображение, то непрерывность функции g на образе f(s) эквивалентна непрерывности g ∘ f на s.
LaTeX
$$$\\text{IsInducing } f \\Rightarrow (\\text{ContinuousOn } g (f'' s) \\iff \\text{ContinuousOn } (g \\circ f) s)$$$
Lean4
/-- If a function is continuous on two closed sets, it is also continuous on their union. -/
theorem union_of_isClosed {f : α → β} (hfs : ContinuousOn f s) (hft : ContinuousOn f t) (hs : IsClosed s)
(ht : IsClosed t) : ContinuousOn f (s ∪ t) :=
by
refine fun x hx ↦ .union ?_ ?_
· refine if hx : x ∈ s then hfs x hx else continuousWithinAt_of_notMem_closure ?_
rwa [hs.closure_eq]
· refine if hx : x ∈ t then hft x hx else continuousWithinAt_of_notMem_closure ?_
rwa [ht.closure_eq]
