of_leftInverse — Mathlib

English

If f:X→Y and g:Y→X are continuous and f∘g = id_Y (i.e., g is a left inverse of f), then g is an embedding.

Русский

Если непрерывны f:X→Y и g:Y→X и f∘g = id_Y, тогда g является вложением.

LaTeX

$$$\text{LeftInverse } f g \Rightarrow \text{Continuous } f, \text{Continuous } g \Rightarrow \text{IsEmbedding } g.$$$

Lean4

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

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