leftInvOn_of_rightInvOn — Mathlib

English

If f is surjective from s onto t and f has a right inverse f' on s, then f has a left inverse on t.

Русский

Если f сюръективна на s → t и f имеет правую обратную f' на s, то на t существует левая обратная к f.

LaTeX

$$$$\\operatorname{SurjOn}(f, s, t) \\land \\operatorname{RightInvOn}(f, f', s) \\Rightarrow \\operatorname{LeftInvOn}(f, f', t).$$$$

Lean4

theorem leftInvOn_of_rightInvOn (hf : SurjOn f s t) (hf' : RightInvOn f f' s) : LeftInvOn f f' t := fun y hy =>
  by
  let ⟨x, hx, heq⟩ := hf hy
  rw [← heq, hf' hx]

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