English
If f: α → β is bijective, then there exists an equivalence α ≃ β given by f, i.e., domain is canonically in bijection with codomain.
Русский
Если f: α → β биекция, то существует эквивалентность α ≃ β, заданная f, то есть множество-область естественным образом корректно сопоставляется кодом.
LaTeX
$$$ \text{If } f: \alpha \to \beta \text{ is bijective, then } \alpha \simeq \beta. $$$
Lean4
/-- If `f` is a bijective function, then its domain is equivalent to its codomain. -/
@[simps (attr := grind =) apply]
noncomputable def ofBijective (f : α → β) (hf : Bijective f) : α ≃ β
where
toFun := f
invFun := surjInv hf.surjective
left_inv := leftInverse_surjInv hf
right_inv := rightInverse_surjInv _
