ofInjective — Mathlib

English

If f is injective, then the resulting equivalence sends x to f(x) as a map.

Русский

Если f инъективен, то полученное эквивалентность отображает x в f(x).

LaTeX

$$$\uparrow(\text{ofInjective } f\; hf\; x) = f(x)$$$

Lean4

/-- Restrict an injective algebra homomorphism to an algebra isomorphism -/
noncomputable def ofInjective (f : A →ₐ[R] B) (hf : Function.Injective f) : A ≃ₐ[R] f.range :=
  ofLeftInverse (Classical.choose_spec hf.hasLeftInverse)

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