English
If s.restrict f is an open map and finv is a left inverse of f on s, then finv is continuous on f''s.
Русский
Если ограничение s.restrict f открытое отображение и finv является левой обратной к f на s, то finv непрерывна на образе f s.
LaTeX
$$$\\text{IsOpenMap } (s.restrict f) \\Rightarrow \\forall \\text{finv},\\ \\text{LeftInvOn } finv f s \\Rightarrow \\text{ContinuousOn } finv (f'' s)$$$
Lean4
theorem continuousOn_image_of_leftInvOn {f : α → β} {s : Set α} (h : IsOpenMap (s.restrict f)) {finv : β → α}
(hleft : LeftInvOn finv f s) : ContinuousOn finv (f '' s) :=
by
refine continuousOn_iff'.2 fun t ht => ⟨f '' (t ∩ s), ?_, ?_⟩
· rw [← image_restrict]
exact h _ (ht.preimage continuous_subtype_val)
· rw [inter_eq_self_of_subset_left (image_mono inter_subset_right), hleft.image_inter']
