localTrivAsPartialEquiv_apply — Mathlib

English

The forward map of the i-th local trivialization sends a point p=(x,v) to (x, coordChange(indexAt x, i, x, v)).

Русский

Передающее отображение i-й локальной тривиализации отправляет точку p=(x,v) в (x, coordChange(indexAt x, i, x, v)).

LaTeX

$$$(\\mathrm{localTrivAsPartialEquiv}\\_i).toFun(p)=(p.1, \\mathrm{coordChange}(\\mathrm{indexAt}(p.1), i, p.1, p.2)).$$$

Lean4

theorem localTrivAsPartialEquiv_apply (p : Z.TotalSpace) :
    (Z.localTrivAsPartialEquiv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ :=
  rfl

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