English
If f' f are inverse-on on sets and f maps s into t as well as f' maps t into s, then f is a bijection from s to t.
Русский
Если f' и f образуют взаимную обратимость на множестве s→t, и f отправляет s в t, а f' отправляет t в s, то f образует биекцию между s и t.
LaTeX
$$$$\\operatorname{InvOn}(f', f, s, t) \\land \\operatorname{MapsTo}(f, s, t) \\land \\operatorname{MapsTo}(f', t, s) \\Rightarrow \\operatorname{BijOn}(f, s, t).$$$$
Lean4
/-- Construct the inverse for a function `f` on domain `s`. This function is a right inverse of `f`
on `f '' s`. For a computable version, see `Function.Embedding.invOfMemRange`. -/
noncomputable def invFunOn [Nonempty α] (f : α → β) (s : Set α) (b : β) : α :=
open scoped Classical in if h : ∃ a, a ∈ s ∧ f a = b then Classical.choose h else Classical.choice ‹Nonempty α›
