ofBijective_apply_symm_apply — Mathlib

English

For a bijection f, the inverse of the equivalence built from f sends f(x) back to x.

Русский

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

LaTeX

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

Lean4

theorem ofBijective_apply_symm_apply (f : α → β) (hf : Bijective f) (x : β) : f ((ofBijective f hf).symm x) = x :=
  (ofBijective f hf).apply_symm_apply x

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