of_inverse — Mathlib

English

If there exists a continuous f' with f' a left inverse and a right inverse of f, then f is a closed map.

Русский

Если существует непрерывное отображение f' с f' — левый и правый обратные к f, то f — замкнутое отображение.

LaTeX

$$$\\exists f'\\,(Continuous f')\\land (f'\\circ f = id) \\land (f\\circ f' = id) \\Rightarrow IsClosedMap(f)$$$

Lean4

theorem of_inverse {f' : Y → X} (h : Continuous f') (l_inv : LeftInverse f f') (r_inv : RightInverse f f') :
    IsClosedMap f := fun s hs => by
  rw [image_eq_preimage_of_inverse r_inv l_inv]
  exact hs.preimage h

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