coordChange_same_apply — Mathlib

English

The fiber coordinate of the fiber coordinate change equals the fiber coordinate of the second trivialization: e1.coordChange e2 b (proj p) . snd = (e2 p).snd.

Русский

Координатный переход по волокну в точке p даёт вторую координату совпадающую с координатой второго тривиализации.

LaTeX

$$$e_1.coordChange e_2 b (proj p)\\!\\, (e_1 p) . snd = (e_2 p) . snd$$$

Lean4

theorem coordChange_same_apply (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) (x : F) :
    e.coordChange e b x = x := by rw [coordChange, e.apply_symm_apply' h]

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