localTriv_symm_fst — Mathlib

English

If b lies in the base sets of both i and j, then the coordinate change along i and j coincides with the local trivialization's coordChangeL at b.

Русский

Если b принадлежит базовым множествам как i, так и j, то переход координат по i и j совпадает с coordChangeL локал-trivialization в точке b.

LaTeX

$$$(Z.localTriv i).coordChangeL(R)\,(Z.localTriv j)\; b\; v = Z.coordChange\; i\; j\; b\; v$ при hb: b ∈ (Z.localTriv i).baseSet ∧ b ∈ (Z.localTriv j).baseSet$$

Lean4

@[simp, mfld_simps]
theorem localTriv_symm_fst (p : B × F) :
    (Z.localTriv i).toOpenPartialHomeomorph.symm p = ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩ :=
  rfl

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