ofBijective_symm_apply_apply — Mathlib

English

For a bijection f, applying the inverse of the induced equivalence to f(x) recovers x.

Русский

Для биекции f применение обратной стороны полученной эквивалентности к f(x) восстанавливает x.

LaTeX

$$$ \forall f (hf : Bijective f) (x:\alpha),\ (Equiv.ofBijective f hf).symm (f x) = x $$$

Lean4

@[simp]
theorem ofBijective_symm_apply_apply (f : α → β) (hf : Bijective f) (x : α) : (ofBijective f hf).symm (f x) = x :=
  (ofBijective f hf).symm_apply_apply x

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