rightInvOn_range — Mathlib

English

If f has a left inverse, then the restricted right inverse on range g maps to the range as a mapping.

Русский

Если есть левый обратный, то ограниченное правое обратное на диапазоне образует отображение в диапазон.

LaTeX

$$$\\text{LeftInverse}\; f\; g \\Rightarrow \\text{RightInvOn}\; f\; g\ (\\text{range } g)$$$

Lean4

theorem rightInvOn_range {g : β → α} (h : LeftInverse f g) : RightInvOn f g (range g) :=
  forall_mem_range.2 fun i => congr_arg g (h i)

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