localTrivAsPartialEquiv_source — Mathlib

English

The source and target of the local trivialization coincide with those of its standard open-structure version.

Русский

Истоки и цели локальной тривиализации совпадают с соответствующими у стандартной открытой версии.

LaTeX

$$$\\mathrm{source}(\\mathcal{L}_i)=\\mathrm{source}((Z.localTriv i))$, $\\mathrm{target}(\\mathcal{L}_i)=\\mathrm{target}((Z.localTriv i))$$$

Lean4

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

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