localTriv_apply — Mathlib

English

Applying the local trivialization to a point in the total space yields the coordinate-pair form (base point, fiber coordinate).

Русский

Применение локальной тривиализации к точке полного пространства даёт пару координат: основание и координату волокна.

LaTeX

$$$(Z.localTriv i).apply(p) = (p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2)$$$

Lean4

@[simp, mfld_simps]
theorem localTriv_apply (p : Z.TotalSpace) : (Z.localTriv i) p = ⟨p.1, Z.coordChange (Z.indexAt p.1) i p.1 p.2⟩ :=
  rfl

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