mem_localTriv_source — Mathlib

English

The second component after applying localTrivAt at b is given by the coordinate-change map from indexAt p.1 to indexAt b.

Русский

Вторая компонента после применения локальной тривиализации в b задаётся координатным изменением от indexAt p.1 к indexAt b.

LaTeX

$$$(Z.localTrivAt b).toFun'(p).snd = Z.coordChange( Z.indexAt p.1, Z.indexAt b) p.1 p.2$$$

Lean4

@[simp, mfld_simps]
theorem mem_localTriv_source (p : Z.TotalSpace) : p ∈ (Z.localTriv i).source ↔ p.1 ∈ (Z.localTriv i).baseSet :=
  Iff.rfl

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