ofBijective_apply_symm_apply — Mathlib

English

Applying the inverse of the promoted isomorphism to f(x) recovers x: (ofBijective f hf).symm (f x) = x.

Русский

Применение обратного к продвинутой эквивалентности к f(x) восстанавливает x: (ofBijective f hf).symm (f x) = x.

LaTeX

$$$ (\\mathrm{ofBijective}(f, hf)).symm (f(x)) = x $$$

Lean4

theorem ofBijective_apply_symm_apply (f : A₁ →ₐ[R] A₂) (hf : Function.Bijective f) (x : A₂) :
    f ((ofBijective f hf).symm x) = x :=
  (ofBijective f hf).apply_symm_apply x

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