continuousOn_range_of_leftInverse

English

If f is an open map and finv is a left inverse of f, then finv is continuous on the range of f.

Русский

Если f открытое отображение и finv — левый обратный к f, то finv непрерывна на области изображения f.

LaTeX

$$$\\text{IsOpenMap } f \\Rightarrow \\forall \\text{finv},\\ \\text{LeftInvOn } finv f \\Rightarrow \\text{ContinuousOn } finv (\\operatorname{range} f)$$$

Lean4

theorem continuousOn_range_of_leftInverse {f : α → β} (hf : IsOpenMap f) {finv : β → α}
    (hleft : Function.LeftInverse finv f) : ContinuousOn finv (range f) :=
  by
  rw [← image_univ]
  exact (hf.restrict isOpen_univ).continuousOn_image_of_leftInvOn fun x _ => hleft x

Похожие утверждения