English
If f' is a right inverse of f on t, and g' is a right inverse of g on p, and g' maps p into t, then the composite f'∘g' is a right inverse of g∘f on p.
Русский
Если f' — правая обратная к f на множестве t, и g' — правая обратная к g на множестве p, и отображение g' отображает p в t, то композиция f'∘g' является правой обратной к композиции g∘f на p.
LaTeX
$$$$\\operatorname{RightInvOn}(f', f, t) \\land \\operatorname{RightInvOn}(g', g, p) \\land \\operatorname{MapsTo}(g', p, t) \\Rightarrow \\operatorname{RightInvOn}(f' \\circ g',\\; g \\circ f,\\; p).$$$$
Lean4
theorem comp (hf : RightInvOn f' f t) (hg : RightInvOn g' g p) (g'pt : MapsTo g' p t) :
RightInvOn (f' ∘ g') (g ∘ f) p :=
LeftInvOn.comp hg hf g'pt
