apply_ofInjective_symm — Mathlib

English

Let f be injective with a left inverse; for any b in the range of f, applying f to the inverse image of b recovers b: f((ofInjective f hf).symm b) = b.

Русский

Пусть f инъективна и существует левый обратный; для любого b из образа f применяя f к обратному образу b восстанавливаем b: f((ofInjective f hf).symm b) = b.

LaTeX

$$$ f((ofInjective\ f\ hf).symm\ b)=b $ для всех $b\\in range(f)$$$

Lean4

theorem apply_ofInjective_symm {α β} {f : α → β} (hf : Injective f) (b : range f) : f ((ofInjective f hf).symm b) = b :=
  Subtype.ext_iff.1 <| (ofInjective f hf).apply_symm_apply b

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