English
Let f be a bijection f : α → β. Then bijInv f_bij is the inverse bijection: it is a function β → α such that f(bijInv f_bij(b)) = b and bijInv f_bij(f(a)) = a.
Русский
Пусть f — биекция α → β. Тогда bijInv f_bij — обратная биекция: она отображает β в α так, что f(bijInv f_bij(b)) = b и bijInv f_bij(f(a)) = a.
LaTeX
$$$\\text{If } f: \\alpha \\to \\beta \\text{ is bijective, then } bijInv(f) : \\beta \\to \\alpha \\text{ is bijective}.$$$
Lean4
/-- `bijInv f` is the unique inverse to a bijection `f`. This acts
as a computable alternative to `Function.invFun`. -/
def bijInv (f_bij : Bijective f) (b : β) : α :=
Fintype.choose (fun a => f a = b) (f_bij.existsUnique b)
