toOpenPartialHomeomorph_left_inv — Mathlib

English

If h is an open embedding f, then the inverse map of the induced open partial homeomorphism sends f(x) back to x for all x in X: (h.toOpenPartialHomeomorph f).symm (f x) = x.

Русский

Если h — открытое вложение f, то обратная карта образованного открытого частичного гомеоморфизма отправляет f(x) в x для всех x в X: (h.toOpenPartialHomeomorph f).symm (f x) = x.

LaTeX

$$$ (h.toOpenPartialHomeomorph f).symm (f x) = x $$$

Lean4

theorem toOpenPartialHomeomorph_left_inv {x : X} : (h.toOpenPartialHomeomorph f).symm (f x) = x :=
  by
  rw [← congr_fun (h.toOpenPartialHomeomorph_apply f), OpenPartialHomeomorph.left_inv]
  exact Set.mem_univ _

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