localTrivAsPartialEquiv_target — Mathlib

English

The symmetric of the local trivialization corresponds to the inverse of the trivialization on the opposite chart.

Русский

Симметричная локальная тривиализация соответствует обратному отображению тривиализации на противоположной карте.

LaTeX

$$$(Z.localTriv i).symm = (Z.localTriv i).toPartialEquiv^{-1}$$$

Lean4

@[simp, mfld_simps]
theorem localTrivAsPartialEquiv_target : (Z.localTrivAsPartialEquiv i).target = (Z.localTriv i).target :=
  rfl

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