ofLeftInverse_symm_apply — Mathlib

English

If f is injective, then the induced algebra equivalence from its restriction to its range is injective on the domain, and conversely.

Русский

Если f инъективен, то соответствующее ограничение до диапазона задаёт инъективное эквивалентное отображение, и наоборот.

LaTeX

$$$\text{Injective}(f) \iff \text{Injective}(\text{ofInjective } f)$$$

Lean4

@[simp]
theorem ofLeftInverse_symm_apply {g : B → A} {f : A →ₐ[R] B} (h : Function.LeftInverse g f) (x : f.range) :
    (ofLeftInverse h).symm x = g x :=
  rfl

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