of_inverse — Mathlib

English

If there exists a global left inverse f' and a right inverse f' with continuity at points, then f is open.

Русский

Если существует глобальная левая обратная функция f' и две стороны обратности, совместимая с непрерывностью, то f открыто.

LaTeX

$$$$\\exists f': Y \\to X, \\text{Continuous } f' \\land LeftInverse\, f\, f' \\land RightInverse\, f\, f' \\rightarrow IsOpenMap(f)$$$$

Lean4

theorem of_inverse {f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f') (r_inv : RightInverse f f') :
    IsOpenMap f :=
  of_sections fun _ => ⟨f', h.continuousAt, r_inv _, l_inv⟩

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