localTrivAsPartialEquiv_symm — Mathlib

English

At a base point, the local trivialization acts as the identity on the base point and fiber coordinate.

Русский

В базовой точке локальная тривиализация действует как тождественная карта на основание и волокно.

LaTeX

$$$(Z.localTrivAt b).apply$ acts as identity at $(b,a)$ for base point $b$ and fiber $a$.$$

Lean4

@[simp, mfld_simps]
theorem localTrivAsPartialEquiv_symm : (Z.localTrivAsPartialEquiv i).symm = (Z.localTriv i).toPartialEquiv.symm :=
  rfl

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