symm_apply_apply — Mathlib

English

For any point x in the source of the pretrivialization, applying the inverse map to the image e(x) yields back x.

Русский

Для любой точки x в области определения предвариационной тривиализации применение обратного отображения к образу e(x) возвращает x.

LaTeX

$$$\forall x\in e.source, e.toPartialEquiv.symm (e x)=x$$$

Lean4

theorem symm_apply_apply {x : Z} (hx : x ∈ e.source) : e.toPartialEquiv.symm (e x) = x :=
  e.toPartialEquiv.left_inv hx

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