of_inverse — Mathlib

English

If f is continuous, g is continuous, and LeftInverse g f, then IsQuotientMap g.

Русский

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

LaTeX

$$$\text{Continuous}(f) \land \text{Continuous}(g) \land \mathrm{LeftInverse}(g,f) \Rightarrow \mathrm{IsQuotientMap}(g)$$$

Lean4

theorem of_inverse {g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : LeftInverse g f) : IsQuotientMap g :=
  .of_comp hf hg <| h.comp_eq_id.symm ▸ IsQuotientMap.id

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