English
If f is injective on s, f has a left inverse f' on t, and f maps s into t while f' maps t into s, then f is invertible on s with f' acting as a right inverse on s.
Русский
Если f инъективна на s, есть левая обратная f' на t, и отображение f отправляет s в t, а отображение f' отправляет t в s, то на s f и f' образуют взаимно обратные функции.
LaTeX
$$$$\\operatorname{InjOn}(f, s) \\land \\operatorname{LeftInvOn}(f, f', t) \\land \\operatorname{MapsTo}(f, s, t) \\land \\operatorname{MapsTo}(f', t, s) \\Rightarrow \\operatorname{RightInvOn}(f, f', s).$$$$
Lean4
theorem rightInvOn_of_leftInvOn (hf : InjOn f s) (hf' : LeftInvOn f f' t) (h₁ : MapsTo f s t) (h₂ : MapsTo f' t s) :
RightInvOn f f' s := fun _ h => hf (h₂ <| h₁ h) h (hf' (h₁ h))
