symm_apply — Mathlib

English

The inverse map for the trivialization is given by the symmetry of the open partial homeomorphism.

Русский

Обратное отображение тривиализации задаётся симметрией соответствующей открытой частичной домашоморфной структуры.

LaTeX

$$$\mathrm{Trivialization.Simps.symm\_apply}(\mathrm{proj}, e) = e.\mathrm{toOpenPartialHomeomorph}.\mathrm{symm}$$$

Lean4

/-- See Note [custom simps projection] -/
noncomputable def symm_apply (proj : Z → B) (e : Trivialization F proj) : B × F → Z :=
  e.toOpenPartialHomeomorph.symm

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