ofInjective — Mathlib

English

If f: α → β is injective, then there exists an equivalence α ≃ range f between α and the range of f.

Русский

Если f: α → β инъективна, то существует эквивалентность между α и образцом range f.

LaTeX

$$$α \\cong range f$$$

Lean4

/-- If `f : α → β` is an injective function, then domain `α` is equivalent to the range of `f`. -/
@[simps! apply]
noncomputable def ofInjective {α β} (f : α → β) (hf : Injective f) : α ≃ range f :=
  Equiv.ofLeftInverse f (fun _ => Function.invFun f) fun _ => Function.leftInverse_invFun hf

Похожие утверждения