English
If f is a bijection between s and t, then invFunOn f s is the inverse pair for f on s and t.
Русский
Если f — биекция между s и t, то invFunOn f s образует взаимно обратное отображение между s и t.
LaTeX
$$$$\\operatorname{BijOn}(f, s, t) \\Rightarrow \\operatorname{InvOn}(\\operatorname{invFunOn} f s, f, s, t).$$$$
Lean4
/-- If functions `f'` and `f` are inverse on `s` and `t`, `f` maps `s` into `t`, and `f'` maps `t`
into `s`, then `f` is a bijection between `s` and `t`. The `mapsTo` arguments can be deduced from
`surjOn` statements using `LeftInvOn.mapsTo` and `RightInvOn.mapsTo`. -/
theorem bijOn (h : InvOn f' f s t) (hf : MapsTo f s t) (hf' : MapsTo f' t s) : BijOn f s t :=
⟨hf, h.left.injOn, h.right.surjOn hf'⟩
