localTrivAt_def — Mathlib

English

A local trivialization of the core registers as a bundle trivialization of the projection, matching the base and fiber data.

Русский

Локальная тривиализация ядра регистрируется как тривиализация биндела проекции, согласующая базовые и волоконные данные.

LaTeX

$$$\\text{localTrivAt}(i) :\\; \\text{Trivialization}(F, \\pi)$ with baseSet = Z.baseSet i, open_source = Z.open_source'(i),\\ toPartialEquiv = Z.localTrivAsPartialEquiv i.$$$

Lean4

@[simp, mfld_simps]
theorem localTrivAt_def (b : B) : Z.localTriv (Z.indexAt b) = Z.localTrivAt b :=
  rfl

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